+
+lemma subst0_gen_lift_rev_ge:
+ \forall (t1: T).(\forall (v: T).(\forall (u2: T).(\forall (i: nat).(\forall
+(h: nat).(\forall (d: nat).((subst0 i v t1 (lift h d u2)) \to ((le (plus d h)
+i) \to (ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 u2)) (\lambda (u1:
+T).(eq T t1 (lift h d u1)))))))))))
+\def
+ \lambda (t1: T).(T_ind (\lambda (t: T).(\forall (v: T).(\forall (u2:
+T).(\forall (i: nat).(\forall (h: nat).(\forall (d: nat).((subst0 i v t (lift
+h d u2)) \to ((le (plus d h) i) \to (ex2 T (\lambda (u1: T).(subst0 (minus i
+h) v u1 u2)) (\lambda (u1: T).(eq T t (lift h d u1)))))))))))) (\lambda (n:
+nat).(\lambda (v: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H: (subst0 i v (TSort n) (lift h d
+u2))).(\lambda (_: (le (plus d h) i)).(subst0_gen_sort v (lift h d u2) i n H
+(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 u2)) (\lambda (u1: T).(eq T
+(TSort n) (lift h d u1))))))))))))) (\lambda (n: nat).(\lambda (v:
+T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (h: nat).(\lambda (d:
+nat).(\lambda (H: (subst0 i v (TLRef n) (lift h d u2))).(\lambda (H0: (le
+(plus d h) i)).(land_ind (eq nat n i) (eq T (lift h d u2) (lift (S n) O v))
+(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 u2)) (\lambda (u1: T).(eq T
+(TLRef n) (lift h d u1)))) (\lambda (H1: (eq nat n i)).(\lambda (H2: (eq T
+(lift h d u2) (lift (S n) O v))).(let H3 \def (eq_ind_r nat i (\lambda (n0:
+nat).(le (plus d h) n0)) H0 n H1) in (eq_ind nat n (\lambda (n0: nat).(ex2 T
+(\lambda (u1: T).(subst0 (minus n0 h) v u1 u2)) (\lambda (u1: T).(eq T (TLRef
+n) (lift h d u1))))) (eq_ind_r nat (plus (minus n h) h) (\lambda (n0:
+nat).(ex2 T (\lambda (u1: T).(subst0 (minus n h) v u1 u2)) (\lambda (u1:
+T).(eq T (TLRef n0) (lift h d u1))))) (eq_ind T (lift h d (TLRef (minus n
+h))) (\lambda (t: T).(ex2 T (\lambda (u1: T).(subst0 (minus n h) v u1 u2))
+(\lambda (u1: T).(eq T t (lift h d u1))))) (let H4 \def (eq_ind nat n
+(\lambda (n0: nat).(eq T (lift h d u2) (lift (S n0) O v))) H2 (plus h (minus
+n h)) (le_plus_minus h n (le_trans h (plus d h) n (le_plus_r d h) H3))) in
+(let H5 \def (eq_ind nat (S (plus h (minus n h))) (\lambda (n0: nat).(eq T
+(lift h d u2) (lift n0 O v))) H4 (plus h (S (minus n h))) (plus_n_Sm h (minus
+n h))) in (let H6 \def (eq_ind_r T (lift (plus h (S (minus n h))) O v)
+(\lambda (t: T).(eq T (lift h d u2) t)) H5 (lift h d (lift (S (minus n h)) O
+v)) (lift_free v (S (minus n h)) h O d (le_S d (minus n h) (le_minus d n h
+H3)) (le_O_n d))) in (eq_ind_r T (lift (S (minus n h)) O v) (\lambda (t:
+T).(ex2 T (\lambda (u1: T).(subst0 (minus n h) v u1 t)) (\lambda (u1: T).(eq
+T (lift h d (TLRef (minus n h))) (lift h d u1))))) (ex_intro2 T (\lambda (u1:
+T).(subst0 (minus n h) v u1 (lift (S (minus n h)) O v))) (\lambda (u1: T).(eq
+T (lift h d (TLRef (minus n h))) (lift h d u1))) (TLRef (minus n h))
+(subst0_lref v (minus n h)) (refl_equal T (lift h d (TLRef (minus n h))))) u2
+(lift_inj u2 (lift (S (minus n h)) O v) h d H6))))) (TLRef (plus (minus n h)
+h)) (lift_lref_ge (minus n h) h d (le_minus d n h H3))) n (le_plus_minus_sym
+h n (le_trans h (plus d h) n (le_plus_r d h) H3))) i H1)))) (subst0_gen_lref
+v (lift h d u2) i n H)))))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H:
+((\forall (v: T).(\forall (u2: T).(\forall (i: nat).(\forall (h:
+nat).(\forall (d: nat).((subst0 i v t (lift h d u2)) \to ((le (plus d h) i)
+\to (ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 u2)) (\lambda (u1:
+T).(eq T t (lift h d u1))))))))))))).(\lambda (t0: T).(\lambda (H0: ((\forall
+(v: T).(\forall (u2: T).(\forall (i: nat).(\forall (h: nat).(\forall (d:
+nat).((subst0 i v t0 (lift h d u2)) \to ((le (plus d h) i) \to (ex2 T
+(\lambda (u1: T).(subst0 (minus i h) v u1 u2)) (\lambda (u1: T).(eq T t0
+(lift h d u1))))))))))))).(\lambda (v: T).(\lambda (u2: T).(\lambda (i:
+nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (subst0 i v (THead k t
+t0) (lift h d u2))).(\lambda (H2: (le (plus d h) i)).(or3_ind (ex2 T (\lambda
+(u3: T).(eq T (lift h d u2) (THead k u3 t0))) (\lambda (u3: T).(subst0 i v t
+u3))) (ex2 T (\lambda (t2: T).(eq T (lift h d u2) (THead k t t2))) (\lambda
+(t2: T).(subst0 (s k i) v t0 t2))) (ex3_2 T T (\lambda (u3: T).(\lambda (t2:
+T).(eq T (lift h d u2) (THead k u3 t2)))) (\lambda (u3: T).(\lambda (_:
+T).(subst0 i v t u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t0
+t2)))) (ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 u2)) (\lambda (u1:
+T).(eq T (THead k t t0) (lift h d u1)))) (\lambda (H3: (ex2 T (\lambda (u3:
+T).(eq T (lift h d u2) (THead k u3 t0))) (\lambda (u3: T).(subst0 i v t
+u3)))).(ex2_ind T (\lambda (u3: T).(eq T (lift h d u2) (THead k u3 t0)))
+(\lambda (u3: T).(subst0 i v t u3)) (ex2 T (\lambda (u1: T).(subst0 (minus i
+h) v u1 u2)) (\lambda (u1: T).(eq T (THead k t t0) (lift h d u1)))) (\lambda
+(x: T).(\lambda (H4: (eq T (lift h d u2) (THead k x t0))).(\lambda (H5:
+(subst0 i v t x)).(let H6 \def (sym_eq T (lift h d u2) (THead k x t0) H4) in
+(let H_x \def (lift_gen_head k x t0 u2 h d H6) in (let H7 \def H_x in
+(ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T u2 (THead k y z))))
+(\lambda (y: T).(\lambda (_: T).(eq T x (lift h d y)))) (\lambda (_:
+T).(\lambda (z: T).(eq T t0 (lift h (s k d) z)))) (ex2 T (\lambda (u1:
+T).(subst0 (minus i h) v u1 u2)) (\lambda (u1: T).(eq T (THead k t t0) (lift
+h d u1)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H8: (eq T u2 (THead k
+x0 x1))).(\lambda (H9: (eq T x (lift h d x0))).(\lambda (H10: (eq T t0 (lift
+h (s k d) x1))).(let H11 \def (eq_ind T x (\lambda (t2: T).(subst0 i v t t2))
+H5 (lift h d x0) H9) in (eq_ind_r T (THead k x0 x1) (\lambda (t2: T).(ex2 T
+(\lambda (u1: T).(subst0 (minus i h) v u1 t2)) (\lambda (u1: T).(eq T (THead
+k t t0) (lift h d u1))))) (eq_ind_r T (lift h (s k d) x1) (\lambda (t2:
+T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 (THead k x0 x1)))
+(\lambda (u1: T).(eq T (THead k t t2) (lift h d u1))))) (let H_x0 \def (H v
+x0 i h d H11 H2) in (let H12 \def H_x0 in (ex2_ind T (\lambda (u1: T).(subst0
+(minus i h) v u1 x0)) (\lambda (u1: T).(eq T t (lift h d u1))) (ex2 T
+(\lambda (u1: T).(subst0 (minus i h) v u1 (THead k x0 x1))) (\lambda (u1:
+T).(eq T (THead k t (lift h (s k d) x1)) (lift h d u1)))) (\lambda (x2:
+T).(\lambda (H13: (subst0 (minus i h) v x2 x0)).(\lambda (H14: (eq T t (lift
+h d x2))).(eq_ind_r T (lift h d x2) (\lambda (t2: T).(ex2 T (\lambda (u1:
+T).(subst0 (minus i h) v u1 (THead k x0 x1))) (\lambda (u1: T).(eq T (THead k
+t2 (lift h (s k d) x1)) (lift h d u1))))) (eq_ind T (lift h d (THead k x2
+x1)) (\lambda (t2: T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 (THead
+k x0 x1))) (\lambda (u1: T).(eq T t2 (lift h d u1))))) (ex_intro2 T (\lambda
+(u1: T).(subst0 (minus i h) v u1 (THead k x0 x1))) (\lambda (u1: T).(eq T
+(lift h d (THead k x2 x1)) (lift h d u1))) (THead k x2 x1) (subst0_fst v x0
+x2 (minus i h) H13 x1 k) (refl_equal T (lift h d (THead k x2 x1)))) (THead k
+(lift h d x2) (lift h (s k d) x1)) (lift_head k x2 x1 h d)) t H14)))) H12)))
+t0 H10) u2 H8))))))) H7))))))) H3)) (\lambda (H3: (ex2 T (\lambda (t2: T).(eq
+T (lift h d u2) (THead k t t2))) (\lambda (t2: T).(subst0 (s k i) v t0
+t2)))).(ex2_ind T (\lambda (t2: T).(eq T (lift h d u2) (THead k t t2)))
+(\lambda (t2: T).(subst0 (s k i) v t0 t2)) (ex2 T (\lambda (u1: T).(subst0
+(minus i h) v u1 u2)) (\lambda (u1: T).(eq T (THead k t t0) (lift h d u1))))
+(\lambda (x: T).(\lambda (H4: (eq T (lift h d u2) (THead k t x))).(\lambda
+(H5: (subst0 (s k i) v t0 x)).(let H6 \def (sym_eq T (lift h d u2) (THead k t
+x) H4) in (let H_x \def (lift_gen_head k t x u2 h d H6) in (let H7 \def H_x
+in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T u2 (THead k y z))))
+(\lambda (y: T).(\lambda (_: T).(eq T t (lift h d y)))) (\lambda (_:
+T).(\lambda (z: T).(eq T x (lift h (s k d) z)))) (ex2 T (\lambda (u1:
+T).(subst0 (minus i h) v u1 u2)) (\lambda (u1: T).(eq T (THead k t t0) (lift
+h d u1)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H8: (eq T u2 (THead k
+x0 x1))).(\lambda (H9: (eq T t (lift h d x0))).(\lambda (H10: (eq T x (lift h
+(s k d) x1))).(let H11 \def (eq_ind T x (\lambda (t2: T).(subst0 (s k i) v t0
+t2)) H5 (lift h (s k d) x1) H10) in (eq_ind_r T (THead k x0 x1) (\lambda (t2:
+T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 t2)) (\lambda (u1: T).(eq
+T (THead k t t0) (lift h d u1))))) (eq_ind_r T (lift h d x0) (\lambda (t2:
+T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 (THead k x0 x1)))
+(\lambda (u1: T).(eq T (THead k t2 t0) (lift h d u1))))) (let H_y \def (H0 v
+x1 (s k i) h (s k d) H11) in (let H12 \def (eq_ind_r nat (plus (s k d) h)
+(\lambda (n: nat).((le n (s k i)) \to (ex2 T (\lambda (u1: T).(subst0 (minus
+(s k i) h) v u1 x1)) (\lambda (u1: T).(eq T t0 (lift h (s k d) u1)))))) H_y
+(s k (plus d h)) (s_plus k d h)) in (let H13 \def (eq_ind_r nat (minus (s k
+i) h) (\lambda (n: nat).((le (s k (plus d h)) (s k i)) \to (ex2 T (\lambda
+(u1: T).(subst0 n v u1 x1)) (\lambda (u1: T).(eq T t0 (lift h (s k d)
+u1)))))) H12 (s k (minus i h)) (s_minus k i h (le_trans h (plus d h) i
+(le_plus_r d h) H2))) in (let H14 \def (H13 (s_le k (plus d h) i H2)) in
+(ex2_ind T (\lambda (u1: T).(subst0 (s k (minus i h)) v u1 x1)) (\lambda (u1:
+T).(eq T t0 (lift h (s k d) u1))) (ex2 T (\lambda (u1: T).(subst0 (minus i h)
+v u1 (THead k x0 x1))) (\lambda (u1: T).(eq T (THead k (lift h d x0) t0)
+(lift h d u1)))) (\lambda (x2: T).(\lambda (H15: (subst0 (s k (minus i h)) v
+x2 x1)).(\lambda (H16: (eq T t0 (lift h (s k d) x2))).(eq_ind_r T (lift h (s
+k d) x2) (\lambda (t2: T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1
+(THead k x0 x1))) (\lambda (u1: T).(eq T (THead k (lift h d x0) t2) (lift h d
+u1))))) (eq_ind T (lift h d (THead k x0 x2)) (\lambda (t2: T).(ex2 T (\lambda
+(u1: T).(subst0 (minus i h) v u1 (THead k x0 x1))) (\lambda (u1: T).(eq T t2
+(lift h d u1))))) (ex_intro2 T (\lambda (u1: T).(subst0 (minus i h) v u1
+(THead k x0 x1))) (\lambda (u1: T).(eq T (lift h d (THead k x0 x2)) (lift h d
+u1))) (THead k x0 x2) (subst0_snd k v x1 x2 (minus i h) H15 x0) (refl_equal T
+(lift h d (THead k x0 x2)))) (THead k (lift h d x0) (lift h (s k d) x2))
+(lift_head k x0 x2 h d)) t0 H16)))) H14))))) t H9) u2 H8))))))) H7)))))))
+H3)) (\lambda (H3: (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T (lift h
+d u2) (THead k u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v t u3)))
+(\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t0 t2))))).(ex3_2_ind T T
+(\lambda (u3: T).(\lambda (t2: T).(eq T (lift h d u2) (THead k u3 t2))))
+(\lambda (u3: T).(\lambda (_: T).(subst0 i v t u3))) (\lambda (_: T).(\lambda
+(t2: T).(subst0 (s k i) v t0 t2))) (ex2 T (\lambda (u1: T).(subst0 (minus i
+h) v u1 u2)) (\lambda (u1: T).(eq T (THead k t t0) (lift h d u1)))) (\lambda
+(x0: T).(\lambda (x1: T).(\lambda (H4: (eq T (lift h d u2) (THead k x0
+x1))).(\lambda (H5: (subst0 i v t x0)).(\lambda (H6: (subst0 (s k i) v t0
+x1)).(let H7 \def (sym_eq T (lift h d u2) (THead k x0 x1) H4) in (let H_x
+\def (lift_gen_head k x0 x1 u2 h d H7) in (let H8 \def H_x in (ex3_2_ind T T
+(\lambda (y: T).(\lambda (z: T).(eq T u2 (THead k y z)))) (\lambda (y:
+T).(\lambda (_: T).(eq T x0 (lift h d y)))) (\lambda (_: T).(\lambda (z:
+T).(eq T x1 (lift h (s k d) z)))) (ex2 T (\lambda (u1: T).(subst0 (minus i h)
+v u1 u2)) (\lambda (u1: T).(eq T (THead k t t0) (lift h d u1)))) (\lambda
+(x2: T).(\lambda (x3: T).(\lambda (H9: (eq T u2 (THead k x2 x3))).(\lambda
+(H10: (eq T x0 (lift h d x2))).(\lambda (H11: (eq T x1 (lift h (s k d)
+x3))).(let H12 \def (eq_ind T x1 (\lambda (t2: T).(subst0 (s k i) v t0 t2))
+H6 (lift h (s k d) x3) H11) in (let H13 \def (eq_ind T x0 (\lambda (t2:
+T).(subst0 i v t t2)) H5 (lift h d x2) H10) in (eq_ind_r T (THead k x2 x3)
+(\lambda (t2: T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1 t2))
+(\lambda (u1: T).(eq T (THead k t t0) (lift h d u1))))) (let H_x0 \def (H v
+x2 i h d H13 H2) in (let H14 \def H_x0 in (ex2_ind T (\lambda (u1: T).(subst0
+(minus i h) v u1 x2)) (\lambda (u1: T).(eq T t (lift h d u1))) (ex2 T
+(\lambda (u1: T).(subst0 (minus i h) v u1 (THead k x2 x3))) (\lambda (u1:
+T).(eq T (THead k t t0) (lift h d u1)))) (\lambda (x: T).(\lambda (H15:
+(subst0 (minus i h) v x x2)).(\lambda (H16: (eq T t (lift h d x))).(eq_ind_r
+T (lift h d x) (\lambda (t2: T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v
+u1 (THead k x2 x3))) (\lambda (u1: T).(eq T (THead k t2 t0) (lift h d u1)))))
+(let H_y \def (H0 v x3 (s k i) h (s k d) H12) in (let H17 \def (eq_ind_r nat
+(plus (s k d) h) (\lambda (n: nat).((le n (s k i)) \to (ex2 T (\lambda (u1:
+T).(subst0 (minus (s k i) h) v u1 x3)) (\lambda (u1: T).(eq T t0 (lift h (s k
+d) u1)))))) H_y (s k (plus d h)) (s_plus k d h)) in (let H18 \def (eq_ind_r
+nat (minus (s k i) h) (\lambda (n: nat).((le (s k (plus d h)) (s k i)) \to
+(ex2 T (\lambda (u1: T).(subst0 n v u1 x3)) (\lambda (u1: T).(eq T t0 (lift h
+(s k d) u1)))))) H17 (s k (minus i h)) (s_minus k i h (le_trans h (plus d h)
+i (le_plus_r d h) H2))) in (let H19 \def (H18 (s_le k (plus d h) i H2)) in
+(ex2_ind T (\lambda (u1: T).(subst0 (s k (minus i h)) v u1 x3)) (\lambda (u1:
+T).(eq T t0 (lift h (s k d) u1))) (ex2 T (\lambda (u1: T).(subst0 (minus i h)
+v u1 (THead k x2 x3))) (\lambda (u1: T).(eq T (THead k (lift h d x) t0) (lift
+h d u1)))) (\lambda (x4: T).(\lambda (H20: (subst0 (s k (minus i h)) v x4
+x3)).(\lambda (H21: (eq T t0 (lift h (s k d) x4))).(eq_ind_r T (lift h (s k
+d) x4) (\lambda (t2: T).(ex2 T (\lambda (u1: T).(subst0 (minus i h) v u1
+(THead k x2 x3))) (\lambda (u1: T).(eq T (THead k (lift h d x) t2) (lift h d
+u1))))) (eq_ind T (lift h d (THead k x x4)) (\lambda (t2: T).(ex2 T (\lambda
+(u1: T).(subst0 (minus i h) v u1 (THead k x2 x3))) (\lambda (u1: T).(eq T t2
+(lift h d u1))))) (ex_intro2 T (\lambda (u1: T).(subst0 (minus i h) v u1
+(THead k x2 x3))) (\lambda (u1: T).(eq T (lift h d (THead k x x4)) (lift h d
+u1))) (THead k x x4) (subst0_both v x x2 (minus i h) H15 k x4 x3 H20)
+(refl_equal T (lift h d (THead k x x4)))) (THead k (lift h d x) (lift h (s k
+d) x4)) (lift_head k x x4 h d)) t0 H21)))) H19))))) t H16)))) H14))) u2
+H9)))))))) H8))))))))) H3)) (subst0_gen_head k v t t0 (lift h d u2) i
+H1)))))))))))))) t1).