X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_lifts.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_lifts.ma;h=2d00bcbc25f3c81330cb0c5d543a7c99f6987ed6;hb=d64b4238ec803353f0a06f2aad25c173852b0526;hp=8477714f3d2c9ff7e30c3b8e2b319523a6bbdb88;hpb=756e320c149ae141dffbf5d75202c8e46c4a49b9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
index 8477714f3..2d00bcbc2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -107,12 +107,12 @@ qed-.
 
 (* Basic_2A1: includes: lift_inj *)
 lemma lifts_inj: ∀f,T1,U. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
-#f #T1 #U #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝  … f)
+#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝  … f)
 /3 width=6 by lifts_div3, lifts_fwd_isid/
 qed-.
 
 (* Basic_2A1: includes: lift_mono *)
 lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
-#f #T #U1 #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝  … f)
+#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝  … f)
 /3 width=6 by lifts_conf, lifts_fwd_isid/
 qed-.