-(t: T).(subst0 i u t x)) H1 (TSort n) (lift_sort n h d)) in (subst0_gen_sort
-u x i n H2 P)))))))))))) (\lambda (n: nat).(\lambda (u: T).(\lambda (x:
-T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (i: 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 (t: T).(subst0 i u t x)) H1
-(TLRef n) (lift_lref_lt n h d H2)) in (and_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 (n: nat).(lt n 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 (t: T).(subst0 i u t
-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 (\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 (n: nat).(lt n (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 n d H6)))))) (subst0_gen_lref u x i
-(plus n h) H3))))))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H:
-((\forall (u: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).(\forall
-(i: nat).((le d i) \to ((lt i (plus d h)) \to ((subst0 i u (lift h d t0) x)
-\to (\forall (P: Prop).P))))))))))).(\lambda (t1: T).(\lambda (H0: ((\forall
-(u: T).(\forall (x: T).(\forall (h: nat).(\forall (d: nat).(\forall (i:
-nat).((le d i) \to ((lt i (plus d h)) \to ((subst0 i u (lift h d t1) x) \to
-(\forall (P: Prop).P))))))))))).(\lambda (u: T).(\lambda (x: T).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (i: nat).(\lambda (H1: (le d i)).(\lambda
-(H2: (lt i (plus d h))).(\lambda (H3: (subst0 i u (lift h d (THead k t0 t1))
-x)).(\lambda (P: Prop).(let H4 \def (eq_ind T (lift h d (THead k t0 t1))
-(\lambda (t: T).(subst0 i u t x)) H3 (THead k (lift h d t0) (lift h (s k d)
-t1)) (lift_head k t0 t1 h d)) in (or3_ind (ex2 T (\lambda (u2: T).(eq T x
-(THead k u2 (lift h (s k d) t1)))) (\lambda (u2: T).(subst0 i u (lift h d t0)
-u2))) (ex2 T (\lambda (t2: T).(eq T x (THead k (lift h d t0) t2))) (\lambda
-(t2: T).(subst0 (s k i) u (lift h (s k d) t1) t2))) (ex3_2 T T (\lambda (u2:
+(t0: T).(subst0 i u t0 x)) H1 (TSort n) (lift_sort n h d)) in
+(subst0_gen_sort u x i n H2 P)))))))))))) (\lambda (n: nat).(\lambda (u:
+T).(\lambda (x: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (i:
+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
+(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
+(\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
+n d H6)))))) (subst0_gen_lref u x i (plus n h) H3))))))))))))))) (\lambda (k:
+K).(\lambda (t0: T).(\lambda (H: ((\forall (u: T).(\forall (x: T).(\forall
+(h: nat).(\forall (d: nat).(\forall (i: nat).((le d i) \to ((lt i (plus d h))
+\to ((subst0 i u (lift h d t0) x) \to (\forall (P:
+Prop).P))))))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (u: T).(\forall
+(x: T).(\forall (h: nat).(\forall (d: nat).(\forall (i: nat).((le d i) \to
+((lt i (plus d h)) \to ((subst0 i u (lift h d t1) x) \to (\forall (P:
+Prop).P))))))))))).(\lambda (u: T).(\lambda (x: T).(\lambda (h: nat).(\lambda
+(d: nat).(\lambda (i: nat).(\lambda (H1: (le d i)).(\lambda (H2: (lt i (plus
+d h))).(\lambda (H3: (subst0 i u (lift h d (THead k t0 t1)) x)).(\lambda (P:
+Prop).(let H4 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda (t2:
+T).(subst0 i u t2 x)) H3 (THead k (lift h d t0) (lift h (s k d) t1))
+(lift_head k t0 t1 h d)) in (or3_ind (ex2 T (\lambda (u2: T).(eq T x (THead k
+u2 (lift h (s k d) t1)))) (\lambda (u2: T).(subst0 i u (lift h d t0) u2)))
+(ex2 T (\lambda (t2: T).(eq T x (THead k (lift h d t0) t2))) (\lambda (t2:
+T).(subst0 (s k i) u (lift h (s k d) t1) t2))) (ex3_2 T T (\lambda (u2: