imp and is_imp need improving

src/LeanSupportEquivalence.v

@@ -415,7 +415,6 @@ Lemma not_is_idle_imp {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList}
     simpl. reflexivity.
   Qed.
 
-
 Lemma not_is_idle_is_imp {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList} 
   (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) 
   (bij_i : permutation i1 i2)
@@ -540,7 +539,7 @@ Lemma not_is_idle_eq {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList}
   apply (not_is_idle_imp b1 b2 bij_i bij_o bij_n bij_e bij_p link_eq).
   apply (not_is_idle_is_imp b1 b2 bij_i bij_o bij_n bij_e bij_p link_eq).
   Qed.
-
+Print not_is_idle_eq.
 
 Theorem support_equivalence_implies_lean_support_equivalence {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList} 
   (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) : 
@@ -553,9 +552,11 @@ Theorem support_equivalence_implies_lean_support_equivalence {s1 r1 s2 r2 : nat}
     (lean b1) (lean b2)
       bij_s bij_i bij_r bij_o 
       bij_n 
-      <{ bij_e | not_is_idle_eq b1 b2 bij_i bij_o bij_n bij_e bij_p link_eq }>
+      <{ bij_e | fun a => conj 
+      (not_is_idle_imp b1 b2 bij_i bij_o bij_n bij_e bij_p link_eq a)
+      (not_is_idle_is_imp b1 b2 bij_i bij_o bij_n bij_e bij_p link_eq a) }>
       bij_p control_eq parent_eq _
-  ).  
+  ).  Check conj.
   clear control_eq parent_eq bij_s bij_r.
   simpl.
   apply functional_extensionality.
@@ -663,4 +664,5 @@ Lemma lean_support_equivalence_trans
     apply support_equivalence_trans.
   Qed.
 
+
 End LeanSupportEquivalence. 
\ No newline at end of file