- "big tree" order implemented

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
index 36c353ba9c75cb1a5d6e694426110fd783927646..ec2cc2df5edcb18e584f4f01675fc07bd825f2c6 100644 (file)
--- 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 tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
 qed-.