T).(eq T x (lift h (S (plus i d)) t2))) (\lambda (t2: T).(subst0 i u (TLRef
n) t2))) (\lambda (H0: (lt n (S (plus i d)))).(let H1 \def (eq_ind T (lift h
(S (plus i d)) (TLRef n)) (\lambda (t: T).(subst0 i (lift h d u) t x)) H
-(TLRef n) (lift_lref_lt n h (S (plus i d)) H0)) in (and_ind (eq nat n i) (eq
+(TLRef n) (lift_lref_lt n h (S (plus i d)) H0)) in (land_ind (eq nat n i) (eq
T x (lift (S n) O (lift h d u))) (ex2 T (\lambda (t2: T).(eq T x (lift h (S
(plus i d)) t2))) (\lambda (t2: T).(subst0 i u (TLRef n) t2))) (\lambda (H2:
(eq nat n i)).(\lambda (H3: (eq T x (lift (S n) O (lift h d u)))).(eq_ind_r T
(subst0_gen_lref (lift h d u) x i n H1)))) (\lambda (H0: (le (S (plus i d))
n)).(let H1 \def (eq_ind T (lift h (S (plus i d)) (TLRef n)) (\lambda (t:
T).(subst0 i (lift h d u) t x)) H (TLRef (plus n h)) (lift_lref_ge n h (S
-(plus i d)) H0)) in (and_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n
+(plus i d)) H0)) in (land_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n
h)) O (lift h d u))) (ex2 T (\lambda (t2: T).(eq T x (lift h (S (plus i d))
t2))) (\lambda (t2: T).(subst0 i u (TLRef n) t2))) (\lambda (H2: (eq nat
(plus n h) i)).(\lambda (_: (eq T x (lift (S (plus n h)) O (lift h d
nat).(\lambda (H: (le d i)).(\lambda (H0: (lt i (plus d h))).(\lambda (H1:
(subst0 i u (lift h d (TLRef n)) x)).(\lambda (P: Prop).(lt_le_e n d P
(\lambda (H2: (lt n d)).(let H3 \def (eq_ind T (lift h d (TLRef n)) (\lambda
-(t0: T).(subst0 i u t0 x)) H1 (TLRef n) (lift_lref_lt n h d H2)) in (and_ind
+(t0: T).(subst0 i u t0 x)) H1 (TLRef n) (lift_lref_lt n h d H2)) in (land_ind
(eq nat n i) (eq T x (lift (S n) O u)) P (\lambda (H4: (eq nat n i)).(\lambda
(_: (eq T x (lift (S n) O u))).(let H6 \def (eq_ind nat n (\lambda (n0:
nat).(lt n0 d)) H2 i H4) in (le_false d i P H H6)))) (subst0_gen_lref u x i n
H3)))) (\lambda (H2: (le d n)).(let H3 \def (eq_ind T (lift h d (TLRef n))
(\lambda (t0: T).(subst0 i u t0 x)) H1 (TLRef (plus n h)) (lift_lref_ge n h d
-H2)) in (and_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n h)) O u)) P
+H2)) in (land_ind (eq nat (plus n h) i) (eq T x (lift (S (plus n h)) O u)) P
(\lambda (H4: (eq nat (plus n h) i)).(\lambda (_: (eq T x (lift (S (plus n
h)) O u))).(let H6 \def (eq_ind_r nat i (\lambda (n0: nat).(lt n0 (plus d
h))) H0 (plus n h) H4) in (le_false d n P H2 (lt_le_S n d (simpl_lt_plus_r h
(t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(subst0 (minus i h) u (TLRef
n) t2))) (\lambda (H1: (lt n d)).(let H2 \def (eq_ind T (lift h d (TLRef n))
(\lambda (t: T).(subst0 i u t x)) H (TLRef n) (lift_lref_lt n h d H1)) in
-(and_ind (eq nat n i) (eq T x (lift (S n) O u)) (ex2 T (\lambda (t2: T).(eq T
-x (lift h d t2))) (\lambda (t2: T).(subst0 (minus i h) u (TLRef n) t2)))
+(land_ind (eq nat n i) (eq T x (lift (S n) O u)) (ex2 T (\lambda (t2: T).(eq
+T x (lift h d t2))) (\lambda (t2: T).(subst0 (minus i h) u (TLRef n) t2)))
(\lambda (H3: (eq nat n i)).(\lambda (_: (eq T x (lift (S n) O u))).(let H5
\def (eq_ind nat n (\lambda (n0: nat).(lt n0 d)) H1 i H3) in (le_false (plus
d h) i (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2:
T).(subst0 (minus i h) u (TLRef n) t2))) H0 (le_plus_trans (S i) d h H5)))))
(subst0_gen_lref u x i n H2)))) (\lambda (H1: (le d n)).(let H2 \def (eq_ind
T (lift h d (TLRef n)) (\lambda (t: T).(subst0 i u t x)) H (TLRef (plus n h))
-(lift_lref_ge n h d H1)) in (and_ind (eq nat (plus n h) i) (eq T x (lift (S
+(lift_lref_ge n h d H1)) in (land_ind (eq nat (plus n h) i) (eq T x (lift (S
(plus n h)) O u)) (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda
(t2: T).(subst0 (minus i h) u (TLRef n) t2))) (\lambda (H3: (eq nat (plus n
h) i)).(\lambda (H4: (eq T x (lift (S (plus n h)) O u))).(eq_ind nat (plus n
h)) O u) t)) (eq_ind_r nat (plus h n) (\lambda (n0: nat).(eq T (lift (S n0) O
u) (lift (plus h (S n)) O u))) (eq_ind_r nat (plus h (S n)) (\lambda (n0:
nat).(eq T (lift n0 O u) (lift (plus h (S n)) O u))) (refl_equal T (lift
-(plus h (S n)) O u)) (S (plus h n)) (plus_n_Sm h n)) (plus n h) (plus_comm n
+(plus h (S n)) O u)) (S (plus h n)) (plus_n_Sm h n)) (plus n h) (plus_sym n
h)) (lift h d (lift (S n) O u)) (lift_free u (S n) h O d (le_trans_plus_r O d
-(plus O (S n)) (plus_le_compat O O d (S n) (le_n O) (le_S d n H1))) (le_O_n
+(plus O (S n)) (le_plus_plus O O d (S n) (le_n O) (le_S d n H1))) (le_O_n
d))) (subst0_lref u n)) (minus (plus n h) h) (minus_plus_r n h)) x H4) i
H3))) (subst0_gen_lref u x i (plus n h) H2)))))))))))) (\lambda (k:
K).(\lambda (t: T).(\lambda (H: ((\forall (x: T).(\forall (i: nat).(\forall