update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / subset_equivalence.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
index bab6b26e1677fa3dbca1f0d37083eb1037c26d8d..b3957eaf304a6079d1dd03c0ccdbbcd9738b40ce 100644 (file)
--- 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 ******************************************************)