renaming in basic_2

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

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 63546ec63c7a402a0117c3467c38d730903199e4..9d7fc61bfee120789fca2059f3d13885132e1c00 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -46,7 +46,7 @@ theorem lifts_div4: ∀f2,Tf,T. ⬆*[f2] Tf ≘ T → ∀g2,Tg. ⬆*[g2] Tg ≘
 ]
 qed-.
 
-lemma lifts_div4_one: â\88\80f,Tf,T. â¬\86*[â\86\91f] Tf ≘ T →
+lemma lifts_div4_one: â\88\80f,Tf,T. â¬\86*[⫯f] Tf ≘ T →
                       ∀T1. ⬆*[1] T1 ≘ T →
                       ∃∃T0. ⬆*[1] T0 ≘ Tf & ⬆*[f] T0 ≘ T1.
 /4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-.