X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_lifts.ma;h=9d7fc61bfee120789fca2059f3d13885132e1c00;hp=63546ec63c7a402a0117c3467c38d730903199e4;hb=222044da28742b24584549ba86b1805a87def070;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d

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 63546ec63..9d7fc61bf 100644
--- 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: ∀f,Tf,T. ⬆*[↑f] Tf ≘ T →
+lemma lifts_div4_one: ∀f,Tf,T. ⬆*[⫯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-.