X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_weight_bind.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_weight_bind.ma;h=3d1bef200566eb91c606564337c8c70a53f988a7;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=62135a02775693683717adc9cb82f25d2acd249e;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_weight_bind.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_weight_bind.ma
index 62135a027..3d1bef200 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_weight_bind.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_weight_bind.ma
@@ -20,6 +20,6 @@ include "static_2/relocation/lifts_bind.ma".
 
 (* Forward lemmas with weight for binders ***********************************)
 
-lemma liftsb_fwd_bw: ∀f,I1,I2. ⬆*[f] I1 ≘ I2 → ♯{I1} = ♯{I2}.
+lemma liftsb_fwd_bw: ∀f,I1,I2. ⇧*[f] I1 ≘ I2 → ♯{I1} = ♯{I2}.
 #f #I1 #I2 * -I1 -I2 /2 width=2 by lifts_fwd_tw/
 qed-.