X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flift.ma;h=7e7961eabe9f4611e081169f8a39ccd3a7061049;hb=c841fac6721efd9ec54ba1ce8479c43ff2389b91;hp=84babbdc8fa8c3fb48b4643952221f93e55b9323;hpb=08cb57944c0df08611d4f35d286e46c0d13e4813;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
index 84babbdc8..7e7961eab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
@@ -276,7 +276,7 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
+lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
 qed-.