X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_lexs.ma;h=a3ff3cdac86b2dc6bf93d54c0457427437e1ec8d;hp=7cfbf82c03a0827e94ea132587c8fa700e3b99ef;hb=268e7f336d036f77ffc9663358e9afda92b97730;hpb=1604f2ee65c57eefb7c6b3122eab2a9f32e0552d

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
index 7cfbf82c0..a3ff3cdac 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
@@ -163,7 +163,7 @@ lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref
                              ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 →
                              ∀b,f,I1,L1. ⬇*[b, f] L1.ⓘ{I1} ≡ K1 →
                              ∀f2. f ~⊚ f1 ≡ ⫯f2 →
-                             ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RN L1 I1 I2 & L1.ⓘ{I1} ≡[f] L2.ⓘ{I2}.
+                             ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RN L1 I1 I2 & L1.ⓘ{I1} ≐[f] L2.ⓘ{I2}.
 #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
 elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
 #X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX
@@ -175,7 +175,7 @@ lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref
                              ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 →
                              ∀b,f,I1,L1. ⬇*[b, f] L1.ⓘ{I1} ≡ K1 →
                              ∀f2. f ~⊚ f1 ≡ ↑f2 →
-                             ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RP L1 I1 I2 & L1.ⓘ{I1} ≡[f] L2.ⓘ{I2}.
+                             ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RP L1 I1 I2 & L1.ⓘ{I1} ≐[f] L2.ⓘ{I2}.
 #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
 elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
 #X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX