X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Fsubset_equivalence.ma;h=b3957eaf304a6079d1dd03c0ccdbbcd9738b40ce;hb=ec5739f16f3d23d26dd2528bf20df21919580e0f;hp=bab6b26e1677fa3dbca1f0d37083eb1037c26d8d;hpb=c8ba3d001893666a52c393d9cf8a0929dacd007a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
index bab6b26e1..b3957eaf3 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/white_harrow_2.ma".
+include "ground/notation/relations/arroweq_2.ma".
 include "ground/lib/subset_inclusion.ma".
 
 (* EQUIVALENCE FOR SUBSETS **************************************************)
@@ -22,7 +22,21 @@ definition subset_eq (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝
 
 interpretation
   "equivalence (subset)"
-  'WhiteHArrow u1 u2 = (subset_eq ? u1 u2).
+  'ArrowEq u1 u2 = (subset_eq ? u1 u2).
+
+(* Basic destructions *******************************************************)
+
+lemma subset_in_eq_repl_back (A) (a:A):
+      ∀u1. a ϵ u1 → ∀u2. u1 ⇔ u2 → a ϵ u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
+
+lemma subset_in_eq_repl_fwd (A) (a:A):
+      ∀u1. a ϵ u1 → ∀u2. u2 ⇔ u1 → a ϵ u2.
+#A #a #u1 #Hu1 #u2 *
+/2 width=1 by/
+qed-.
 
 (* Basic constructions ******************************************************)