updating the dropable-related definitions with coafter ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_lreq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
index 2ce496bd50887c1b28f525e48a0a7a476f4ddbe7..48520094936473ebd8fc46e68f56534d57f3ff4e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
@@ -30,7 +30,7 @@ lemma lreq_dropable: ∀RN,RP. dropable_dx (lexs RN RP).
 (* Basic_2A1: includes: lreq_drop_trans_be *)
 lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 →
                              ∀b,f,I,K2,V. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V → 𝐔⦃f⦄ →
-                             ∀f1. f ⊚ ⫯f1 ≡ f2 →
+                             ∀f1. f ~⊚ ⫯f1 ≡ f2 →
                              ∃∃K1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V & K1 ≡[f1] K2.
 #f2 #L1 #L2 #HL12 #b #f #I #K1 #V #HLK1 #Hf #f1 #Hf2
 elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -f2 -L2 -Hf
@@ -40,7 +40,7 @@ qed-.
 (* Basic_2A1: includes: lreq_drop_conf_be *)
 lemma lreq_drops_conf_next: ∀f2,L1,L2. L1 ≡[f2] L2 →
                             ∀b,f,I,K1,V. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V → 𝐔⦃f⦄ →
-                            ∀f1. f ⊚ ⫯f1 ≡ f2 →
+                            ∀f1. f ~⊚ ⫯f1 ≡ f2 →
                             ∃∃K2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V & K1 ≡[f1] K2.
 #f2 #L1 #L2 #HL12 #b #f #I #K1 #V #HLK1 #Hf #f1 #Hf2
 elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -f2 -L1 -Hf
@@ -49,7 +49,7 @@ qed-.
 
 lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 →
                              ∀b,f,I,L1,V. ⬇*[b,f] L1.ⓑ{I}V ≡ K1 →
-                             ∀f2. f ⊚ f1 ≡ ⫯f2 →
+                             ∀f2. f ~⊚ f1 ≡ ⫯f2 →
                              ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V≡[f]L2.ⓑ{I}V.
 #f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1