nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TSort n) (TSort
n))).(\lambda (P: Prop).(subst0_gen_sort u (TSort n) d n H P))))) (\lambda
(n: nat).(\lambda (d: nat).(\lambda (H: (subst0 d u (TLRef n) (TLRef
-n))).(\lambda (P: Prop).(and_ind (eq nat n d) (eq T (TLRef n) (lift (S n) O
+n))).(\lambda (P: Prop).(land_ind (eq nat n d) (eq T (TLRef n) (lift (S n) O
u)) P (\lambda (_: (eq nat n d)).(\lambda (H1: (eq T (TLRef n) (lift (S n) O
u))).(lift_gen_lref_false (S n) O n (le_O_n n) (le_n (plus O (S n))) u H1
P))) (subst0_gen_lref u (TLRef n) d n H)))))) (\lambda (k: K).(\lambda (t0:
(plus i0 h) v (TLRef (plus i0 h)) t)) (eq_ind nat (S (plus h i0)) (\lambda
(n: nat).(subst0 (plus i0 h) v (TLRef (plus i0 h)) (lift n O v))) (eq_ind_r
nat (plus h i0) (\lambda (n: nat).(subst0 n v (TLRef n) (lift (S (plus h i0))
-O v))) (subst0_lref v (plus h i0)) (plus i0 h) (plus_comm i0 h)) (plus h (S
+O v))) (subst0_lref v (plus h i0)) (plus i0 h) (plus_sym i0 h)) (plus h (S
i0)) (plus_n_Sm h i0)) (lift h d (lift (S i0) O v)) (lift_free v (S i0) h O d
(le_S d i0 H0) (le_O_n d))) (lift h d (TLRef i0)) (lift_lref_ge i0 h d
H0)))))) (\lambda (v: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0:
(plus i (S O)) (\lambda (n: nat).(subst0 n u (lift (S O) d t1) (lift (S O) d
t2))) (subst0_lift_ge t1 t2 u i (S O) H d H0) (S i) (eq_ind_r nat (plus (S O)
i) (\lambda (n: nat).(eq nat n (S i))) (refl_equal nat (S i)) (plus i (S O))
-(plus_comm i (S O)))))))))).
+(plus_sym i (S O)))))))))).
theorem subst0_lift_ge_s:
\forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0