]
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
(* 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-.
#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 *********************************************************)
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