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=bcc1db8b27d6507df839049d2576d036b303a65b;hpb=fba384e357ed3c8781fc018c2c16f2b40df144af;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 bcc1db8b2..7e7961eab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
@@ -259,6 +259,7 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → ⊥.
 ]
 qed-.
 
+(* Basic_1: was: thead_x_lift_y_y *)
 lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → ⊥.
 #J #T elim T -T
 [ * #i #V #d #e #H
@@ -275,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-.
 
@@ -289,7 +290,7 @@ lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒⦃T2⦄ → 
 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
 #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
 elim (simple_inv_bind … H)
-qed-. 
+qed-.
 
 (* Basic properties *********************************************************)
 
@@ -393,7 +394,7 @@ lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R)
   elim (IHU1 … HTU1) -U1 #T #HTU #HT1
   elim (HR … HU2 … HTU) -U /3 width=5/
 ]
-qed-. 
+qed-.
 
 (* Basic_1: removed theorems 7:
             lift_head lift_gen_head