lse in a equiv

src/LeanSupportEquivalence.v

@@ -754,7 +754,7 @@ Theorem support_equivalence_implies_lean_support_equivalence {s1 r1 s2 r2 : nat}
 Theorem lean_support_equivalence_refl {s r : nat} {i o : b.n.NoDupList} (b : bigraph s i r o) :
   lean_support_equivalence b b.
   Proof. 
-    apply support_equivalence_implies_lean_support_equivalence.
+    unfold lean_support_equivalence.
     apply support_equivalence_refl.
   Qed.
 
@@ -764,10 +764,9 @@ Lemma lean_support_equivalence_sym {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : b.n.NoDupL
   lean_support_equivalence b1 b2
       -> lean_support_equivalence b2 b1.
   Proof.
-    intros. 
-    apply support_equivalence_implies_lean_support_equivalence.
+    unfold lean_support_equivalence.
     apply support_equivalence_sym.
-  Admitted.
+  Qed.
 
 Lemma lean_support_equivalence_trans 
   {s1 r1 s2 r2 s3 r3 : nat} {i1 o1 i2 o2 i3 o3: b.n.NoDupList} 
@@ -776,7 +775,8 @@ Lemma lean_support_equivalence_trans
       -> lean_support_equivalence b2 b3  
         -> lean_support_equivalence b1 b3.
   Proof.
-  Admitted.
-
+    unfold lean_support_equivalence.
+    apply support_equivalence_trans.
+  Qed.
 
 End LeanSupportEquivalence. 
\ No newline at end of file