X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_lifts.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_lifts.ma;h=3f78beb36186a076a15bf13b79ad588c68a8ec09;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=3aef874bc1731e436318e7234529f3d340c50287;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
index 3aef874bc..3f78beb36 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
@@ -112,13 +112,13 @@ qed-.
 
 (* Basic_2A1: includes: lift_inj *)
 lemma lifts_inj: ∀f. is_inj2 … (lifts f).
-#f #T1 #U #H1 #T2 #H2 lapply (after_isid_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. is_mono … (lifts f T).
-#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝  … f)
+#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐢  … f)
 /3 width=6 by lifts_conf, lifts_fwd_isid/
 qed-.