lse pas trop trivial l'equivalence

src/LeanSupportEquivalence.v

@@ -751,4 +751,32 @@ Theorem support_equivalence_implies_lean_support_equivalence {s1 r1 s2 r2 : nat}
   Qed.
 
 
+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.
+    apply support_equivalence_refl.
+  Qed.
+
+
+Lemma lean_support_equivalence_sym {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : b.n.NoDupList}  
+  (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) :
+  lean_support_equivalence b1 b2
+      -> lean_support_equivalence b2 b1.
+  Proof.
+    intros. 
+    apply support_equivalence_implies_lean_support_equivalence.
+    apply support_equivalence_sym.
+  Admitted.
+
+Lemma lean_support_equivalence_trans 
+  {s1 r1 s2 r2 s3 r3 : nat} {i1 o1 i2 o2 i3 o3: b.n.NoDupList} 
+  (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) (b3 : bigraph s3 i3 r3 o3):
+    lean_support_equivalence b1 b2
+      -> lean_support_equivalence b2 b3  
+        -> lean_support_equivalence b1 b3.
+  Proof.
+  Admitted.
+
+
 End LeanSupportEquivalence. 
\ No newline at end of file