we exported some inversors from coq

[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / subst0 / fwd.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma
index bb669667e086638ba368c43ca6e4d6f2dc49f679..622fbc20d9b97a09f90e3dd1bef19a36bb84e12b 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma
@@ -20,135 +20,194 @@ include "subst0/defs.ma".
 
 include "lift/props.ma".
 
+theorem subst0_inv_coq:
+ \forall (i: nat).(\forall (v: T).(\forall (t1: T).(\forall (t2: T).(\forall 
+(P: ((nat \to (T \to (T \to (T \to Prop)))))).((((subst0 i v t1 t2) \to 
+(\forall (v0: T).(\forall (i0: nat).((eq nat i0 i) \to ((eq T v0 v) \to ((eq 
+T (TLRef i0) t1) \to ((eq T (lift (S i0) O v0) t2) \to (P i v t1 t2))))))))) 
+\to ((((subst0 i v t1 t2) \to (\forall (v0: T).(\forall (u2: T).(\forall (u1: 
+T).(\forall (i0: nat).(\forall (t: T).(\forall (k: K).((eq nat i0 i) \to ((eq 
+T v0 v) \to ((eq T (THead k u1 t) t1) \to ((eq T (THead k u2 t) t2) \to 
+((subst0 i0 v0 u1 u2) \to (P i v t1 t2)))))))))))))) \to ((((subst0 i v t1 
+t2) \to (\forall (k: K).(\forall (v0: T).(\forall (t0: T).(\forall (t3: 
+T).(\forall (i0: nat).(\forall (u: T).((eq nat i0 i) \to ((eq T v0 v) \to 
+((eq T (THead k u t3) t1) \to ((eq T (THead k u t0) t2) \to ((subst0 (s k i0) 
+v0 t3 t0) \to (P i v t1 t2)))))))))))))) \to ((((subst0 i v t1 t2) \to 
+(\forall (v0: T).(\forall (u1: T).(\forall (u2: T).(\forall (i0: 
+nat).(\forall (k: K).(\forall (t0: T).(\forall (t3: T).((eq nat i0 i) \to 
+((eq T v0 v) \to ((eq T (THead k u1 t0) t1) \to ((eq T (THead k u2 t3) t2) 
+\to ((subst0 i0 v0 u1 u2) \to ((subst0 (s k i0) v0 t0 t3) \to (P i v t1 
+t2)))))))))))))))) \to ((subst0 i v t1 t2) \to (P i v t1 t2))))))))))
+\def
+ \lambda (i: nat).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
+(P: ((nat \to (T \to (T \to (T \to Prop)))))).(\lambda (H: (((subst0 i v t1 
+t2) \to (\forall (v0: T).(\forall (i0: nat).((eq nat i0 i) \to ((eq T v0 v) 
+\to ((eq T (TLRef i0) t1) \to ((eq T (lift (S i0) O v0) t2) \to (P i v t1 
+t2)))))))))).(\lambda (H0: (((subst0 i v t1 t2) \to (\forall (v0: T).(\forall 
+(u2: T).(\forall (u1: T).(\forall (i0: nat).(\forall (t: T).(\forall (k: 
+K).((eq nat i0 i) \to ((eq T v0 v) \to ((eq T (THead k u1 t) t1) \to ((eq T 
+(THead k u2 t) t2) \to ((subst0 i0 v0 u1 u2) \to (P i v t1 
+t2))))))))))))))).(\lambda (H1: (((subst0 i v t1 t2) \to (\forall (k: 
+K).(\forall (v0: T).(\forall (t0: T).(\forall (t3: T).(\forall (i0: 
+nat).(\forall (u: T).((eq nat i0 i) \to ((eq T v0 v) \to ((eq T (THead k u 
+t3) t1) \to ((eq T (THead k u t0) t2) \to ((subst0 (s k i0) v0 t3 t0) \to (P 
+i v t1 t2))))))))))))))).(\lambda (H2: (((subst0 i v t1 t2) \to (\forall (v0: 
+T).(\forall (u1: T).(\forall (u2: T).(\forall (i0: nat).(\forall (k: 
+K).(\forall (t0: T).(\forall (t3: T).((eq nat i0 i) \to ((eq T v0 v) \to ((eq 
+T (THead k u1 t0) t1) \to ((eq T (THead k u2 t3) t2) \to ((subst0 i0 v0 u1 
+u2) \to ((subst0 (s k i0) v0 t0 t3) \to (P i v t1 
+t2))))))))))))))))).(\lambda (H3: (subst0 i v t1 t2)).(let H4 \def (match H3 
+in subst0 return (\lambda (n: nat).(\lambda (t: T).(\lambda (t0: T).(\lambda 
+(t3: T).(\lambda (_: (subst0 n t t0 t3)).((eq nat n i) \to ((eq T t v) \to 
+((eq T t0 t1) \to ((eq T t3 t2) \to (P i v t1 t2)))))))))) with [(subst0_lref 
+v0 i0) \Rightarrow (\lambda (H4: (eq nat i0 i)).(\lambda (H5: (eq T v0 
+v)).(\lambda (H6: (eq T (TLRef i0) t1)).(\lambda (H7: (eq T (lift (S i0) O 
+v0) t2)).(H H3 v0 i0 H4 H5 H6 H7))))) | (subst0_fst v0 u2 u1 i0 H4 t k) 
+\Rightarrow (\lambda (H5: (eq nat i0 i)).(\lambda (H6: (eq T v0 v)).(\lambda 
+(H7: (eq T (THead k u1 t) t1)).(\lambda (H8: (eq T (THead k u2 t) t2)).(H0 H3 
+v0 u2 u1 i0 t k H5 H6 H7 H8 H4))))) | (subst0_snd k v0 t0 t3 i0 H4 u) 
+\Rightarrow (\lambda (H5: (eq nat i0 i)).(\lambda (H6: (eq T v0 v)).(\lambda 
+(H7: (eq T (THead k u t3) t1)).(\lambda (H8: (eq T (THead k u t0) t2)).(H1 H3 
+k v0 t0 t3 i0 u H5 H6 H7 H8 H4))))) | (subst0_both v0 u1 u2 i0 H4 k t0 t3 H5) 
+\Rightarrow (\lambda (H6: (eq nat i0 i)).(\lambda (H7: (eq T v0 v)).(\lambda 
+(H8: (eq T (THead k u1 t0) t1)).(\lambda (H9: (eq T (THead k u2 t3) t2)).(H2 
+H3 v0 u1 u2 i0 k t0 t3 H6 H7 H8 H9 H4 H5)))))]) in (H4 (refl_equal nat i) 
+(refl_equal T v) (refl_equal T t1) (refl_equal T t2)))))))))))).
+
 theorem subst0_gen_sort:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst0 
 i v (TSort n) x) \to (\forall (P: Prop).P)))))
 \def
  \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda 
-(H: (subst0 i v (TSort n) x)).(\lambda (P: Prop).(let H0 \def (match H in 
-subst0 return (\lambda (n0: nat).(\lambda (t: T).(\lambda (t0: T).(\lambda 
-(t1: T).(\lambda (_: (subst0 n0 t t0 t1)).((eq nat n0 i) \to ((eq T t v) \to 
-((eq T t0 (TSort n)) \to ((eq T t1 x) \to P))))))))) with [(subst0_lref v0 
-i0) \Rightarrow (\lambda (H0: (eq nat i0 i)).(\lambda (H1: (eq T v0 
-v)).(\lambda (H2: (eq T (TLRef i0) (TSort n))).(\lambda (H3: (eq T (lift (S 
-i0) O v0) x)).(eq_ind nat i (\lambda (n0: nat).((eq T v0 v) \to ((eq T (TLRef 
-n0) (TSort n)) \to ((eq T (lift (S n0) O v0) x) \to P)))) (\lambda (H4: (eq T 
-v0 v)).(eq_ind T v (\lambda (t: T).((eq T (TLRef i) (TSort n)) \to ((eq T 
-(lift (S i) O t) x) \to P))) (\lambda (H5: (eq T (TLRef i) (TSort n))).(let 
-H6 \def (eq_ind T (TLRef i) (\lambda (e: T).(match e in T return (\lambda (_: 
+(H: (subst0 i v (TSort n) x)).(\lambda (P: Prop).(subst0_inv_coq i v (TSort 
+n) x (\lambda (_: nat).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).P)))) 
+(\lambda (H0: (subst0 i v (TSort n) x)).(\lambda (v0: T).(\lambda (i0: 
+nat).(\lambda (H1: (eq nat i0 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: 
+(eq T (TLRef i0) (TSort n))).(\lambda (H4: (eq T (lift (S i0) O v0) x)).(let 
+H5 \def (eq_ind nat i0 (\lambda (n0: nat).(eq T (lift (S n0) O v0) x)) H4 i 
+H1) in (let H6 \def (eq_ind nat i0 (\lambda (n0: nat).(eq T (TLRef n0) (TSort 
+n))) H3 i H1) in (let H7 \def (eq_ind T v0 (\lambda (t: T).(eq T (lift (S i) 
+O t) x)) H5 v H2) in (let H8 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v 
+(TSort n) t)) H0 (lift (S i) O v) H7) in (let H9 \def (eq_ind_r T x (\lambda 
+(t: T).(subst0 i v (TSort n) t)) H (lift (S i) O v) H7) in (let H10 \def 
+(eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (TSort n) H5) in (False_ind ((eq T (lift 
-(S i) O v) x) \to P) H6))) v0 (sym_eq T v0 v H4))) i0 (sym_eq nat i0 i H0) H1 
-H2 H3))))) | (subst0_fst v0 u2 u1 i0 H0 t k) \Rightarrow (\lambda (H1: (eq 
-nat i0 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k u1 t) 
-(TSort n))).(\lambda (H4: (eq T (THead k u2 t) x)).(eq_ind nat i (\lambda 
-(n0: nat).((eq T v0 v) \to ((eq T (THead k u1 t) (TSort n)) \to ((eq T (THead 
-k u2 t) x) \to ((subst0 n0 v0 u1 u2) \to P))))) (\lambda (H5: (eq T v0 
-v)).(eq_ind T v (\lambda (t0: T).((eq T (THead k u1 t) (TSort n)) \to ((eq T 
-(THead k u2 t) x) \to ((subst0 i t0 u1 u2) \to P)))) (\lambda (H6: (eq T 
-(THead k u1 t) (TSort n))).(let H7 \def (eq_ind T (THead k u1 t) (\lambda (e: 
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
-(TSort n) H6) in (False_ind ((eq T (THead k u2 t) x) \to ((subst0 i v u1 u2) 
-\to P)) H7))) v0 (sym_eq T v0 v H5))) i0 (sym_eq nat i0 i H1) H2 H3 H4 
-H0))))) | (subst0_snd k v0 t2 t1 i0 H0 u) \Rightarrow (\lambda (H1: (eq nat 
-i0 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k u t1) (TSort 
-n))).(\lambda (H4: (eq T (THead k u t2) x)).(eq_ind nat i (\lambda (n0: 
-nat).((eq T v0 v) \to ((eq T (THead k u t1) (TSort n)) \to ((eq T (THead k u 
-t2) x) \to ((subst0 (s k n0) v0 t1 t2) \to P))))) (\lambda (H5: (eq T v0 
-v)).(eq_ind T v (\lambda (t: T).((eq T (THead k u t1) (TSort n)) \to ((eq T 
-(THead k u t2) x) \to ((subst0 (s k i) t t1 t2) \to P)))) (\lambda (H6: (eq T 
-(THead k u t1) (TSort n))).(let H7 \def (eq_ind T (THead k u t1) (\lambda (e: 
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
-(TSort n) H6) in (False_ind ((eq T (THead k u t2) x) \to ((subst0 (s k i) v 
-t1 t2) \to P)) H7))) v0 (sym_eq T v0 v H5))) i0 (sym_eq nat i0 i H1) H2 H3 H4 
-H0))))) | (subst0_both v0 u1 u2 i0 H0 k t1 t2 H1) \Rightarrow (\lambda (H2: 
-(eq nat i0 i)).(\lambda (H3: (eq T v0 v)).(\lambda (H4: (eq T (THead k u1 t1) 
-(TSort n))).(\lambda (H5: (eq T (THead k u2 t2) x)).(eq_ind nat i (\lambda 
-(n0: nat).((eq T v0 v) \to ((eq T (THead k u1 t1) (TSort n)) \to ((eq T 
-(THead k u2 t2) x) \to ((subst0 n0 v0 u1 u2) \to ((subst0 (s k n0) v0 t1 t2) 
-\to P)))))) (\lambda (H6: (eq T v0 v)).(eq_ind T v (\lambda (t: T).((eq T 
-(THead k u1 t1) (TSort n)) \to ((eq T (THead k u2 t2) x) \to ((subst0 i t u1 
-u2) \to ((subst0 (s k i) t t1 t2) \to P))))) (\lambda (H7: (eq T (THead k u1 
-t1) (TSort n))).(let H8 \def (eq_ind T (THead k u1 t1) (\lambda (e: T).(match 
-e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
+(THead _ _ _) \Rightarrow False])) I (TSort n) H6) in (False_ind P 
+H10)))))))))))))) (\lambda (H0: (subst0 i v (TSort n) x)).(\lambda (v0: 
+T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0: nat).(\lambda (t: 
+T).(\lambda (k: K).(\lambda (H1: (eq nat i0 i)).(\lambda (H2: (eq T v0 
+v)).(\lambda (H3: (eq T (THead k u1 t) (TSort n))).(\lambda (H4: (eq T (THead 
+k u2 t) x)).(\lambda (H5: (subst0 i0 v0 u1 u2)).(let H6 \def (eq_ind nat i0 
+(\lambda (n0: nat).(subst0 n0 v0 u1 u2)) H5 i H1) in (let H7 \def (eq_ind T 
+v0 (\lambda (t0: T).(subst0 i t0 u1 u2)) H6 v H2) in (let H8 \def (eq_ind_r T 
+x (\lambda (t0: T).(subst0 i v (TSort n) t0)) H0 (THead k u2 t) H4) in (let 
+H9 \def (eq_ind_r T x (\lambda (t0: T).(subst0 i v (TSort n) t0)) H (THead k 
+u2 t) H4) in (let H10 \def (eq_ind T (THead k u1 t) (\lambda (ee: T).(match 
+ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) 
-H7) in (False_ind ((eq T (THead k u2 t2) x) \to ((subst0 i v u1 u2) \to 
-((subst0 (s k i) v t1 t2) \to P))) H8))) v0 (sym_eq T v0 v H6))) i0 (sym_eq 
-nat i0 i H2) H3 H4 H5 H0 H1)))))]) in (H0 (refl_equal nat i) (refl_equal T v) 
-(refl_equal T (TSort n)) (refl_equal T x)))))))).
+H3) in (False_ind P H10)))))))))))))))))) (\lambda (H0: (subst0 i v (TSort n) 
+x)).(\lambda (k: K).(\lambda (v0: T).(\lambda (t0: T).(\lambda (t3: 
+T).(\lambda (i0: nat).(\lambda (u: T).(\lambda (H1: (eq nat i0 i)).(\lambda 
+(H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k u t3) (TSort n))).(\lambda 
+(H4: (eq T (THead k u t0) x)).(\lambda (H5: (subst0 (s k i0) v0 t3 t0)).(let 
+H6 \def (eq_ind nat i0 (\lambda (n0: nat).(subst0 (s k n0) v0 t3 t0)) H5 i 
+H1) in (let H7 \def (eq_ind T v0 (\lambda (t: T).(subst0 (s k i) t t3 t0)) H6 
+v H2) in (let H8 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v (TSort n) t)) 
+H0 (THead k u t0) H4) in (let H9 \def (eq_ind_r T x (\lambda (t: T).(subst0 i 
+v (TSort n) t)) H (THead k u t0) H4) in (let H10 \def (eq_ind T (THead k u 
+t3) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
+_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
+\Rightarrow True])) I (TSort n) H3) in (False_ind P H10)))))))))))))))))) 
+(\lambda (H0: (subst0 i v (TSort n) x)).(\lambda (v0: T).(\lambda (u1: 
+T).(\lambda (u2: T).(\lambda (i0: nat).(\lambda (k: K).(\lambda (t0: 
+T).(\lambda (t3: T).(\lambda (H2: (eq nat i0 i)).(\lambda (H3: (eq T v0 
+v)).(\lambda (H4: (eq T (THead k u1 t0) (TSort n))).(\lambda (H5: (eq T 
+(THead k u2 t3) x)).(\lambda (H1: (subst0 i0 v0 u1 u2)).(\lambda (H6: (subst0 
+(s k i0) v0 t0 t3)).(let H7 \def (eq_ind nat i0 (\lambda (n0: nat).(subst0 (s 
+k n0) v0 t0 t3)) H6 i H2) in (let H8 \def (eq_ind nat i0 (\lambda (n0: 
+nat).(subst0 n0 v0 u1 u2)) H1 i H2) in (let H9 \def (eq_ind T v0 (\lambda (t: 
+T).(subst0 (s k i) t t0 t3)) H7 v H3) in (let H10 \def (eq_ind T v0 (\lambda 
+(t: T).(subst0 i t u1 u2)) H8 v H3) in (let H11 \def (eq_ind_r T x (\lambda 
+(t: T).(subst0 i v (TSort n) t)) H0 (THead k u2 t3) H5) in (let H12 \def 
+(eq_ind_r T x (\lambda (t: T).(subst0 i v (TSort n) t)) H (THead k u2 t3) H5) 
+in (let H13 \def (eq_ind T (THead k u1 t0) (\lambda (ee: T).(match ee in T 
+return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H4) in 
+(False_ind P H13)))))))))))))))))))))) H)))))).
 
 theorem subst0_gen_lref:
  \forall (v: T).(\forall (x: T).(\forall (i: nat).(\forall (n: nat).((subst0 
 i v (TLRef n) x) \to (land (eq nat n i) (eq T x (lift (S n) O v)))))))
 \def
  \lambda (v: T).(\lambda (x: T).(\lambda (i: nat).(\lambda (n: nat).(\lambda 
-(H: (subst0 i v (TLRef n) x)).(let H0 \def (match H in subst0 return (\lambda 
-(n0: nat).(\lambda (t: T).(\lambda (t0: T).(\lambda (t1: T).(\lambda (_: 
-(subst0 n0 t t0 t1)).((eq nat n0 i) \to ((eq T t v) \to ((eq T t0 (TLRef n)) 
-\to ((eq T t1 x) \to (land (eq nat n i) (eq T x (lift (S n) O v)))))))))))) 
-with [(subst0_lref v0 i0) \Rightarrow (\lambda (H0: (eq nat i0 i)).(\lambda 
-(H1: (eq T v0 v)).(\lambda (H2: (eq T (TLRef i0) (TLRef n))).(\lambda (H3: 
-(eq T (lift (S i0) O v0) x)).(eq_ind nat i (\lambda (n0: nat).((eq T v0 v) 
-\to ((eq T (TLRef n0) (TLRef n)) \to ((eq T (lift (S n0) O v0) x) \to (land 
-(eq nat n i) (eq T x (lift (S n) O v))))))) (\lambda (H4: (eq T v0 
-v)).(eq_ind T v (\lambda (t: T).((eq T (TLRef i) (TLRef n)) \to ((eq T (lift 
-(S i) O t) x) \to (land (eq nat n i) (eq T x (lift (S n) O v)))))) (\lambda 
-(H5: (eq T (TLRef i) (TLRef n))).(let H6 \def (f_equal T nat (\lambda (e: 
-T).(match e in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | 
-(TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef 
-n) H5) in (eq_ind nat n (\lambda (n0: nat).((eq T (lift (S n0) O v) x) \to 
-(land (eq nat n n0) (eq T x (lift (S n) O v))))) (\lambda (H7: (eq T (lift (S 
-n) O v) x)).(eq_ind T (lift (S n) O v) (\lambda (t: T).(land (eq nat n n) (eq 
-T t (lift (S n) O v)))) (conj (eq nat n n) (eq T (lift (S n) O v) (lift (S n) 
-O v)) (refl_equal nat n) (refl_equal T (lift (S n) O v))) x H7)) i (sym_eq 
-nat i n H6)))) v0 (sym_eq T v0 v H4))) i0 (sym_eq nat i0 i H0) H1 H2 H3))))) 
-| (subst0_fst v0 u2 u1 i0 H0 t k) \Rightarrow (\lambda (H1: (eq nat i0 
-i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k u1 t) (TLRef 
-n))).(\lambda (H4: (eq T (THead k u2 t) x)).(eq_ind nat i (\lambda (n0: 
-nat).((eq T v0 v) \to ((eq T (THead k u1 t) (TLRef n)) \to ((eq T (THead k u2 
-t) x) \to ((subst0 n0 v0 u1 u2) \to (land (eq nat n i) (eq T x (lift (S n) O 
-v)))))))) (\lambda (H5: (eq T v0 v)).(eq_ind T v (\lambda (t0: T).((eq T 
-(THead k u1 t) (TLRef n)) \to ((eq T (THead k u2 t) x) \to ((subst0 i t0 u1 
-u2) \to (land (eq nat n i) (eq T x (lift (S n) O v))))))) (\lambda (H6: (eq T 
-(THead k u1 t) (TLRef n))).(let H7 \def (eq_ind T (THead k u1 t) (\lambda (e: 
-T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I 
-(TLRef n) H6) in (False_ind ((eq T (THead k u2 t) x) \to ((subst0 i v u1 u2) 
-\to (land (eq nat n i) (eq T x (lift (S n) O v))))) H7))) v0 (sym_eq T v0 v 
-H5))) i0 (sym_eq nat i0 i H1) H2 H3 H4 H0))))) | (subst0_snd k v0 t2 t1 i0 H0 
-u) \Rightarrow (\lambda (H1: (eq nat i0 i)).(\lambda (H2: (eq T v0 
-v)).(\lambda (H3: (eq T (THead k u t1) (TLRef n))).(\lambda (H4: (eq T (THead 
-k u t2) x)).(eq_ind nat i (\lambda (n0: nat).((eq T v0 v) \to ((eq T (THead k 
-u t1) (TLRef n)) \to ((eq T (THead k u t2) x) \to ((subst0 (s k n0) v0 t1 t2) 
-\to (land (eq nat n i) (eq T x (lift (S n) O v)))))))) (\lambda (H5: (eq T v0 
-v)).(eq_ind T v (\lambda (t: T).((eq T (THead k u t1) (TLRef n)) \to ((eq T 
-(THead k u t2) x) \to ((subst0 (s k i) t t1 t2) \to (land (eq nat n i) (eq T 
-x (lift (S n) O v))))))) (\lambda (H6: (eq T (THead k u t1) (TLRef n))).(let 
-H7 \def (eq_ind T (THead k u t1) (\lambda (e: T).(match e in T return 
+(H: (subst0 i v (TLRef n) x)).(subst0_inv_coq i v (TLRef n) x (\lambda (n0: 
+nat).(\lambda (t: T).(\lambda (_: T).(\lambda (t1: T).(land (eq nat n n0) (eq 
+T t1 (lift (S n) O t))))))) (\lambda (H0: (subst0 i v (TLRef n) x)).(\lambda 
+(v0: T).(\lambda (i0: nat).(\lambda (H1: (eq nat i0 i)).(\lambda (H2: (eq T 
+v0 v)).(\lambda (H3: (eq T (TLRef i0) (TLRef n))).(\lambda (H4: (eq T (lift 
+(S i0) O v0) x)).(let H5 \def (eq_ind nat i0 (\lambda (n0: nat).(eq T (lift 
+(S n0) O v0) x)) H4 i H1) in (let H6 \def (eq_ind nat i0 (\lambda (n0: 
+nat).(eq T (TLRef n0) (TLRef n))) H3 i H1) in (let H7 \def (eq_ind T v0 
+(\lambda (t: T).(eq T (lift (S i) O t) x)) H5 v H2) in (let H8 \def (eq_ind_r 
+T x (\lambda (t: T).(subst0 i v (TLRef n) t)) H0 (lift (S i) O v) H7) in (let 
+H9 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v (TLRef n) t)) H (lift (S i) 
+O v) H7) in (eq_ind T (lift (S i) O v) (\lambda (t: T).(land (eq nat n i) (eq 
+T t (lift (S n) O v)))) (let H10 \def (f_equal T nat (\lambda (e: T).(match e 
+in T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | (TLRef n0) 
+\Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n) H6) in 
+(let H11 \def (eq_ind_r nat n (\lambda (n0: nat).(subst0 i v (TLRef n0) (lift 
+(S i) O v))) H8 i H10) in (let H12 \def (eq_ind_r nat n (\lambda (n0: 
+nat).(subst0 i v (TLRef n0) (lift (S i) O v))) H9 i H10) in (eq_ind nat i 
+(\lambda (n0: nat).(land (eq nat n0 i) (eq T (lift (S i) O v) (lift (S n0) O 
+v)))) (conj (eq nat i i) (eq T (lift (S i) O v) (lift (S i) O v)) (refl_equal 
+nat i) (refl_equal T (lift (S i) O v))) n H10)))) x H7))))))))))))) (\lambda 
+(H0: (subst0 i v (TLRef n) x)).(\lambda (v0: T).(\lambda (u2: T).(\lambda 
+(u1: T).(\lambda (i0: nat).(\lambda (t: T).(\lambda (k: K).(\lambda (H1: (eq 
+nat i0 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k u1 t) 
+(TLRef n))).(\lambda (H4: (eq T (THead k u2 t) x)).(\lambda (H5: (subst0 i0 
+v0 u1 u2)).(let H6 \def (eq_ind nat i0 (\lambda (n0: nat).(subst0 n0 v0 u1 
+u2)) H5 i H1) in (let H7 \def (eq_ind T v0 (\lambda (t0: T).(subst0 i t0 u1 
+u2)) H6 v H2) in (let H8 \def (eq_ind_r T x (\lambda (t0: T).(subst0 i v 
+(TLRef n) t0)) H0 (THead k u2 t) H4) in (let H9 \def (eq_ind_r T x (\lambda 
+(t0: T).(subst0 i v (TLRef n) t0)) H (THead k u2 t) H4) in (eq_ind T (THead k 
+u2 t) (\lambda (t0: T).(land (eq nat n i) (eq T t0 (lift (S n) O v)))) (let 
+H10 \def (eq_ind T (THead k u1 t) (\lambda (ee: T).(match ee in T return 
 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H6) in 
-(False_ind ((eq T (THead k u t2) x) \to ((subst0 (s k i) v t1 t2) \to (land 
-(eq nat n i) (eq T x (lift (S n) O v))))) H7))) v0 (sym_eq T v0 v H5))) i0 
-(sym_eq nat i0 i H1) H2 H3 H4 H0))))) | (subst0_both v0 u1 u2 i0 H0 k t1 t2 
-H1) \Rightarrow (\lambda (H2: (eq nat i0 i)).(\lambda (H3: (eq T v0 
-v)).(\lambda (H4: (eq T (THead k u1 t1) (TLRef n))).(\lambda (H5: (eq T 
-(THead k u2 t2) x)).(eq_ind nat i (\lambda (n0: nat).((eq T v0 v) \to ((eq T 
-(THead k u1 t1) (TLRef n)) \to ((eq T (THead k u2 t2) x) \to ((subst0 n0 v0 
-u1 u2) \to ((subst0 (s k n0) v0 t1 t2) \to (land (eq nat n i) (eq T x (lift 
-(S n) O v))))))))) (\lambda (H6: (eq T v0 v)).(eq_ind T v (\lambda (t: 
-T).((eq T (THead k u1 t1) (TLRef n)) \to ((eq T (THead k u2 t2) x) \to 
-((subst0 i t u1 u2) \to ((subst0 (s k i) t t1 t2) \to (land (eq nat n i) (eq 
-T x (lift (S n) O v)))))))) (\lambda (H7: (eq T (THead k u1 t1) (TLRef 
-n))).(let H8 \def (eq_ind T (THead k u1 t1) (\lambda (e: T).(match e in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H7) in 
-(False_ind ((eq T (THead k u2 t2) x) \to ((subst0 i v u1 u2) \to ((subst0 (s 
-k i) v t1 t2) \to (land (eq nat n i) (eq T x (lift (S n) O v)))))) H8))) v0 
-(sym_eq T v0 v H6))) i0 (sym_eq nat i0 i H2) H3 H4 H5 H0 H1)))))]) in (H0 
-(refl_equal nat i) (refl_equal T v) (refl_equal T (TLRef n)) (refl_equal T 
-x))))))).
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H3) in 
+(False_ind (land (eq nat n i) (eq T (THead k u2 t) (lift (S n) O v))) H10)) x 
+H4))))))))))))))))) (\lambda (H0: (subst0 i v (TLRef n) x)).(\lambda (k: 
+K).(\lambda (v0: T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i0: 
+nat).(\lambda (u: T).(\lambda (H1: (eq nat i0 i)).(\lambda (H2: (eq T v0 
+v)).(\lambda (H3: (eq T (THead k u t3) (TLRef n))).(\lambda (H4: (eq T (THead 
+k u t0) x)).(\lambda (H5: (subst0 (s k i0) v0 t3 t0)).(let H6 \def (eq_ind 
+nat i0 (\lambda (n0: nat).(subst0 (s k n0) v0 t3 t0)) H5 i H1) in (let H7 
+\def (eq_ind T v0 (\lambda (t: T).(subst0 (s k i) t t3 t0)) H6 v H2) in (let 
+H8 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v (TLRef n) t)) H0 (THead k u 
+t0) H4) in (let H9 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v (TLRef n) 
+t)) H (THead k u t0) H4) in (eq_ind T (THead k u t0) (\lambda (t: T).(land 
+(eq nat n i) (eq T t (lift (S n) O v)))) (let H10 \def (eq_ind T (THead k u 
+t3) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
+_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
+\Rightarrow True])) I (TLRef n) H3) in (False_ind (land (eq nat n i) (eq T 
+(THead k u t0) (lift (S n) O v))) H10)) x H4))))))))))))))))) (\lambda (H0: 
+(subst0 i v (TLRef n) x)).(\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: 
+T).(\lambda (i0: nat).(\lambda (k: K).(\lambda (t0: T).(\lambda (t3: 
+T).(\lambda (H2: (eq nat i0 i)).(\lambda (H3: (eq T v0 v)).(\lambda (H4: (eq 
+T (THead k u1 t0) (TLRef n))).(\lambda (H5: (eq T (THead k u2 t3) 
+x)).(\lambda (H1: (subst0 i0 v0 u1 u2)).(\lambda (H6: (subst0 (s k i0) v0 t0 
+t3)).(let H7 \def (eq_ind nat i0 (\lambda (n0: nat).(subst0 (s k n0) v0 t0 
+t3)) H6 i H2) in (let H8 \def (eq_ind nat i0 (\lambda (n0: nat).(subst0 n0 v0 
+u1 u2)) H1 i H2) in (let H9 \def (eq_ind T v0 (\lambda (t: T).(subst0 (s k i) 
+t t0 t3)) H7 v H3) in (let H10 \def (eq_ind T v0 (\lambda (t: T).(subst0 i t 
+u1 u2)) H8 v H3) in (let H11 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v 
+(TLRef n) t)) H0 (THead k u2 t3) H5) in (let H12 \def (eq_ind_r T x (\lambda 
+(t: T).(subst0 i v (TLRef n) t)) H (THead k u2 t3) H5) in (eq_ind T (THead k 
+u2 t3) (\lambda (t: T).(land (eq nat n i) (eq T t (lift (S n) O v)))) (let 
+H13 \def (eq_ind T (THead k u1 t0) (\lambda (ee: T).(match ee in T return 
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H4) in 
+(False_ind (land (eq nat n i) (eq T (THead k u2 t3) (lift (S n) O v))) H13)) 
+x H5))))))))))))))))))))) H))))).
 
 theorem subst0_gen_head:
  \forall (k: K).(\forall (v: T).(\forall (u1: T).(\forall (t1: T).(\forall 
@@ -160,236 +219,191 @@ T).(eq T x (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1
 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))))))))
 \def
  \lambda (k: K).(\lambda (v: T).(\lambda (u1: T).(\lambda (t1: T).(\lambda 
-(x: T).(\lambda (i: nat).(\lambda (H: (subst0 i v (THead k u1 t1) x)).(let H0 
-\def (match H in subst0 return (\lambda (n: nat).(\lambda (t: T).(\lambda 
-(t0: T).(\lambda (t2: T).(\lambda (_: (subst0 n t t0 t2)).((eq nat n i) \to 
-((eq T t v) \to ((eq T t0 (THead k u1 t1)) \to ((eq T t2 x) \to (or3 (ex2 T 
-(\lambda (u2: T).(eq T x (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 
-u2))) (ex2 T (\lambda (t3: T).(eq T x (THead k u1 t3))) (\lambda (t3: 
-T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: 
-T).(eq T x (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 
-u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))))))))))))) 
-with [(subst0_lref v0 i0) \Rightarrow (\lambda (H0: (eq nat i0 i)).(\lambda 
-(H1: (eq T v0 v)).(\lambda (H2: (eq T (TLRef i0) (THead k u1 t1))).(\lambda 
-(H3: (eq T (lift (S i0) O v0) x)).(eq_ind nat i (\lambda (n: nat).((eq T v0 
-v) \to ((eq T (TLRef n) (THead k u1 t1)) \to ((eq T (lift (S n) O v0) x) \to 
-(or3 (ex2 T (\lambda (u2: T).(eq T x (THead k u2 t1))) (\lambda (u2: 
-T).(subst0 i v u1 u2))) (ex2 T (\lambda (t2: T).(eq T x (THead k u1 t2))) 
-(\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u2: 
-T).(\lambda (t2: T).(eq T x (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: 
-T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 
-t2))))))))) (\lambda (H4: (eq T v0 v)).(eq_ind T v (\lambda (t: T).((eq T 
-(TLRef i) (THead k u1 t1)) \to ((eq T (lift (S i) O t) x) \to (or3 (ex2 T 
-(\lambda (u2: T).(eq T x (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 
-u2))) (ex2 T (\lambda (t2: T).(eq T x (THead k u1 t2))) (\lambda (t2: 
-T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2: 
-T).(eq T x (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 
-u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))))) 
-(\lambda (H5: (eq T (TLRef i) (THead k u1 t1))).(let H6 \def (eq_ind T (TLRef 
-i) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) 
+(x: T).(\lambda (i: nat).(\lambda (H: (subst0 i v (THead k u1 t1) 
+x)).(subst0_inv_coq i v (THead k u1 t1) x (\lambda (n: nat).(\lambda (t: 
+T).(\lambda (_: T).(\lambda (t2: T).(or3 (ex2 T (\lambda (u2: T).(eq T t2 
+(THead k u2 t1))) (\lambda (u2: T).(subst0 n t u1 u2))) (ex2 T (\lambda (t3: 
+T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k n) t t1 t3))) 
+(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 n t u1 u2))) (\lambda (_: 
+T).(\lambda (t3: T).(subst0 (s k n) t t1 t3))))))))) (\lambda (H0: (subst0 i 
+v (THead k u1 t1) x)).(\lambda (v0: T).(\lambda (i0: nat).(\lambda (H1: (eq 
+nat i0 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (TLRef i0) (THead k 
+u1 t1))).(\lambda (H4: (eq T (lift (S i0) O v0) x)).(let H5 \def (eq_ind nat 
+i0 (\lambda (n: nat).(eq T (lift (S n) O v0) x)) H4 i H1) in (let H6 \def 
+(eq_ind nat i0 (\lambda (n: nat).(eq T (TLRef n) (THead k u1 t1))) H3 i H1) 
+in (let H7 \def (eq_ind T v0 (\lambda (t: T).(eq T (lift (S i) O t) x)) H5 v 
+H2) in (let H8 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v (THead k u1 t1) 
+t)) H0 (lift (S i) O v) H7) in (let H9 \def (eq_ind_r T x (\lambda (t: 
+T).(subst0 i v (THead k u1 t1) t)) H (lift (S i) O v) H7) in (eq_ind T (lift 
+(S i) O v) (\lambda (t: T).(or3 (ex2 T (\lambda (u2: T).(eq T t (THead k u2 
+t1))) (\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t2: T).(eq T t 
+(THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T 
+(\lambda (u2: T).(\lambda (t2: T).(eq T t (THead k u2 t2)))) (\lambda (u2: 
+T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t2: 
+T).(subst0 (s k i) v t1 t2)))))) (let H10 \def (eq_ind T (TLRef i) (\lambda 
+(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
-False])) I (THead k u1 t1) H5) in (False_ind ((eq T (lift (S i) O v) x) \to 
-(or3 (ex2 T (\lambda (u2: T).(eq T x (THead k u2 t1))) (\lambda (u2: 
-T).(subst0 i v u1 u2))) (ex2 T (\lambda (t2: T).(eq T x (THead k u1 t2))) 
-(\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u2: 
-T).(\lambda (t2: T).(eq T x (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: 
+False])) I (THead k u1 t1) H6) in (False_ind (or3 (ex2 T (\lambda (u2: T).(eq 
+T (lift (S i) O v) (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))) 
+(ex2 T (\lambda (t2: T).(eq T (lift (S i) O v) (THead k u1 t2))) (\lambda 
+(t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2: 
+T).(eq T (lift (S i) O v) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: 
 T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 
-t2)))))) H6))) v0 (sym_eq T v0 v H4))) i0 (sym_eq nat i0 i H0) H1 H2 H3))))) 
-| (subst0_fst v0 u2 u0 i0 H0 t k0) \Rightarrow (\lambda (H1: (eq nat i0 
-i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k0 u0 t) (THead k 
-u1 t1))).(\lambda (H4: (eq T (THead k0 u2 t) x)).(eq_ind nat i (\lambda (n: 
-nat).((eq T v0 v) \to ((eq T (THead k0 u0 t) (THead k u1 t1)) \to ((eq T 
-(THead k0 u2 t) x) \to ((subst0 n v0 u0 u2) \to (or3 (ex2 T (\lambda (u3: 
-T).(eq T x (THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T 
-(\lambda (t2: T).(eq T x (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v 
-t1 t2))) (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T x (THead k u3 
-t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
-T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))))))) (\lambda (H5: (eq T v0 
-v)).(eq_ind T v (\lambda (t0: T).((eq T (THead k0 u0 t) (THead k u1 t1)) \to 
-((eq T (THead k0 u2 t) x) \to ((subst0 i t0 u0 u2) \to (or3 (ex2 T (\lambda 
-(u3: T).(eq T x (THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 
-T (\lambda (t2: T).(eq T x (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) 
-v t1 t2))) (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T x (THead k u3 
-t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
-T).(\lambda (t2: T).(subst0 (s k i) v t1 t2))))))))) (\lambda (H6: (eq T 
-(THead k0 u0 t) (THead k u1 t1))).(let H7 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t | 
-(TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0])) (THead k0 u0 t) 
-(THead k u1 t1) H6) in ((let H8 \def (f_equal T T (\lambda (e: T).(match e in 
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) 
-\Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead k0 u0 t) (THead k u1 
-t1) H6) in ((let H9 \def (f_equal T K (\lambda (e: T).(match e in T return 
-(\lambda (_: T).K) with [(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 
-| (THead k1 _ _) \Rightarrow k1])) (THead k0 u0 t) (THead k u1 t1) H6) in 
-(eq_ind K k (\lambda (k1: K).((eq T u0 u1) \to ((eq T t t1) \to ((eq T (THead 
-k1 u2 t) x) \to ((subst0 i v u0 u2) \to (or3 (ex2 T (\lambda (u3: T).(eq T x 
-(THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: 
-T).(eq T x (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) 
-(ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T x (THead k u3 t2)))) 
-(\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
-T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))))))) (\lambda (H10: (eq T u0 
-u1)).(eq_ind T u1 (\lambda (t0: T).((eq T t t1) \to ((eq T (THead k u2 t) x) 
-\to ((subst0 i v t0 u2) \to (or3 (ex2 T (\lambda (u3: T).(eq T x (THead k u3 
-t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq T x 
+t2))))) H10)) x H7))))))))))))) (\lambda (H0: (subst0 i v (THead k u1 t1) 
+x)).(\lambda (v0: T).(\lambda (u2: T).(\lambda (u0: T).(\lambda (i0: 
+nat).(\lambda (t: T).(\lambda (k0: K).(\lambda (H1: (eq nat i0 i)).(\lambda 
+(H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k0 u0 t) (THead k u1 
+t1))).(\lambda (H4: (eq T (THead k0 u2 t) x)).(\lambda (H5: (subst0 i0 v0 u0 
+u2)).(let H6 \def (eq_ind nat i0 (\lambda (n: nat).(subst0 n v0 u0 u2)) H5 i 
+H1) in (let H7 \def (eq_ind T v0 (\lambda (t0: T).(subst0 i t0 u0 u2)) H6 v 
+H2) in (let H8 \def (eq_ind_r T x (\lambda (t0: T).(subst0 i v (THead k u1 
+t1) t0)) H0 (THead k0 u2 t) H4) in (let H9 \def (eq_ind_r T x (\lambda (t0: 
+T).(subst0 i v (THead k u1 t1) t0)) H (THead k0 u2 t) H4) in (eq_ind T (THead 
+k0 u2 t) (\lambda (t0: T).(or3 (ex2 T (\lambda (u3: T).(eq T t0 (THead k u3 
+t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq T t0 
 (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T 
-(\lambda (u3: T).(\lambda (t2: T).(eq T x (THead k u3 t2)))) (\lambda (u3: 
-T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: 
-T).(subst0 (s k i) v t1 t2))))))))) (\lambda (H11: (eq T t t1)).(eq_ind T t1 
-(\lambda (t0: T).((eq T (THead k u2 t0) x) \to ((subst0 i v u1 u2) \to (or3 
-(ex2 T (\lambda (u3: T).(eq T x (THead k u3 t1))) (\lambda (u3: T).(subst0 i 
-v u1 u3))) (ex2 T (\lambda (t2: T).(eq T x (THead k u1 t2))) (\lambda (t2: 
-T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u3: T).(\lambda (t2: 
-T).(eq T x (THead k u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 
-u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))))) 
-(\lambda (H12: (eq T (THead k u2 t1) x)).(eq_ind T (THead k u2 t1) (\lambda 
-(t0: T).((subst0 i v u1 u2) \to (or3 (ex2 T (\lambda (u3: T).(eq T t0 (THead 
-k u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq 
-T t0 (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T 
 (\lambda (u3: T).(\lambda (t2: T).(eq T t0 (THead k u3 t2)))) (\lambda (u3: 
 T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: 
-T).(subst0 (s k i) v t1 t2))))))) (\lambda (H13: (subst0 i v u1 
-u2)).(or3_intro0 (ex2 T (\lambda (u3: T).(eq T (THead k u2 t1) (THead k u3 
-t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq T 
-(THead k u2 t1) (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) 
-(ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead k u2 t1) (THead k 
-u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
-T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))) (ex_intro2 T (\lambda (u3: 
-T).(eq T (THead k u2 t1) (THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 
-u3)) u2 (refl_equal T (THead k u2 t1)) H13))) x H12)) t (sym_eq T t t1 H11))) 
-u0 (sym_eq T u0 u1 H10))) k0 (sym_eq K k0 k H9))) H8)) H7))) v0 (sym_eq T v0 
-v H5))) i0 (sym_eq nat i0 i H1) H2 H3 H4 H0))))) | (subst0_snd k0 v0 t2 t0 i0 
-H0 u) \Rightarrow (\lambda (H1: (eq nat i0 i)).(\lambda (H2: (eq T v0 
-v)).(\lambda (H3: (eq T (THead k0 u t0) (THead k u1 t1))).(\lambda (H4: (eq T 
-(THead k0 u t2) x)).(eq_ind nat i (\lambda (n: nat).((eq T v0 v) \to ((eq T 
-(THead k0 u t0) (THead k u1 t1)) \to ((eq T (THead k0 u t2) x) \to ((subst0 
-(s k0 n) v0 t0 t2) \to (or3 (ex2 T (\lambda (u2: T).(eq T x (THead k u2 t1))) 
-(\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t3: T).(eq T x (THead 
-k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda 
-(u2: T).(\lambda (t3: T).(eq T x (THead k u2 t3)))) (\lambda (u2: T).(\lambda 
-(_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) 
-v t1 t3)))))))))) (\lambda (H5: (eq T v0 v)).(eq_ind T v (\lambda (t: T).((eq 
-T (THead k0 u t0) (THead k u1 t1)) \to ((eq T (THead k0 u t2) x) \to ((subst0 
-(s k0 i) t t0 t2) \to (or3 (ex2 T (\lambda (u2: T).(eq T x (THead k u2 t1))) 
-(\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t3: T).(eq T x (THead 
-k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda 
-(u2: T).(\lambda (t3: T).(eq T x (THead k u2 t3)))) (\lambda (u2: T).(\lambda 
-(_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) 
-v t1 t3))))))))) (\lambda (H6: (eq T (THead k0 u t0) (THead k u1 t1))).(let 
-H7 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
-with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) 
-\Rightarrow t])) (THead k0 u t0) (THead k u1 t1) H6) in ((let H8 \def 
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
-[(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) 
-\Rightarrow t])) (THead k0 u t0) (THead k u1 t1) H6) in ((let H9 \def 
-(f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K) with 
-[(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _ _) 
-\Rightarrow k1])) (THead k0 u t0) (THead k u1 t1) H6) in (eq_ind K k (\lambda 
-(k1: K).((eq T u u1) \to ((eq T t0 t1) \to ((eq T (THead k1 u t2) x) \to 
-((subst0 (s k1 i) v t0 t2) \to (or3 (ex2 T (\lambda (u2: T).(eq T x (THead k 
-u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t3: T).(eq T 
-x (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T 
-(\lambda (u2: T).(\lambda (t3: T).(eq T x (THead k u2 t3)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3: 
-T).(subst0 (s k i) v t1 t3)))))))))) (\lambda (H10: (eq T u u1)).(eq_ind T u1 
-(\lambda (t: T).((eq T t0 t1) \to ((eq T (THead k t t2) x) \to ((subst0 (s k 
-i) v t0 t2) \to (or3 (ex2 T (\lambda (u2: T).(eq T x (THead k u2 t1))) 
-(\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t3: T).(eq T x (THead 
-k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda 
-(u2: T).(\lambda (t3: T).(eq T x (THead k u2 t3)))) (\lambda (u2: T).(\lambda 
-(_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) 
-v t1 t3))))))))) (\lambda (H11: (eq T t0 t1)).(eq_ind T t1 (\lambda (t: 
-T).((eq T (THead k u1 t2) x) \to ((subst0 (s k i) v t t2) \to (or3 (ex2 T 
-(\lambda (u2: T).(eq T x (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 
-u2))) (ex2 T (\lambda (t3: T).(eq T x (THead k u1 t3))) (\lambda (t3: 
-T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: 
-T).(eq T x (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 
-u2))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))))))) 
-(\lambda (H12: (eq T (THead k u1 t2) x)).(eq_ind T (THead k u1 t2) (\lambda 
-(t: T).((subst0 (s k i) v t1 t2) \to (or3 (ex2 T (\lambda (u2: T).(eq T t 
-(THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t3: 
-T).(eq T t (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) 
-(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead k u2 t3)))) 
+T).(subst0 (s k i) v t1 t2)))))) (let H10 \def (f_equal T K (\lambda (e: 
+T).(match e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k0 | 
+(TLRef _) \Rightarrow k0 | (THead k1 _ _) \Rightarrow k1])) (THead k0 u0 t) 
+(THead k u1 t1) H3) in ((let H11 \def (f_equal T T (\lambda (e: T).(match e 
+in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) 
+\Rightarrow u0 | (THead _ t0 _) \Rightarrow t0])) (THead k0 u0 t) (THead k u1 
+t1) H3) in ((let H12 \def (f_equal T T (\lambda (e: T).(match e in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow t | (TLRef _) \Rightarrow t | 
+(THead _ _ t0) \Rightarrow t0])) (THead k0 u0 t) (THead k u1 t1) H3) in 
+(\lambda (H13: (eq T u0 u1)).(\lambda (H14: (eq K k0 k)).(let H15 \def 
+(eq_ind K k0 (\lambda (k1: K).(subst0 i v (THead k u1 t1) (THead k1 u2 t))) 
+H9 k H14) in (let H16 \def (eq_ind K k0 (\lambda (k1: K).(subst0 i v (THead k 
+u1 t1) (THead k1 u2 t))) H8 k H14) in (eq_ind_r K k (\lambda (k1: K).(or3 
+(ex2 T (\lambda (u3: T).(eq T (THead k1 u2 t) (THead k u3 t1))) (\lambda (u3: 
+T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq T (THead k1 u2 t) (THead 
+k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda 
+(u3: T).(\lambda (t2: T).(eq T (THead k1 u2 t) (THead k u3 t2)))) (\lambda 
+(u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: 
+T).(subst0 (s k i) v t1 t2)))))) (let H17 \def (eq_ind T t (\lambda (t0: 
+T).(subst0 i v (THead k u1 t1) (THead k u2 t0))) H15 t1 H12) in (let H18 \def 
+(eq_ind T t (\lambda (t0: T).(subst0 i v (THead k u1 t1) (THead k u2 t0))) 
+H16 t1 H12) in (eq_ind_r T t1 (\lambda (t0: T).(or3 (ex2 T (\lambda (u3: 
+T).(eq T (THead k u2 t0) (THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 
+u3))) (ex2 T (\lambda (t2: T).(eq T (THead k u2 t0) (THead k u1 t2))) 
+(\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u3: 
+T).(\lambda (t2: T).(eq T (THead k u2 t0) (THead k u3 t2)))) (\lambda (u3: 
+T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: 
+T).(subst0 (s k i) v t1 t2)))))) (let H19 \def (eq_ind T u0 (\lambda (t0: 
+T).(subst0 i v t0 u2)) H7 u1 H13) in (or3_intro0 (ex2 T (\lambda (u3: T).(eq 
+T (THead k u2 t1) (THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) 
+(ex2 T (\lambda (t2: T).(eq T (THead k u2 t1) (THead k u1 t2))) (\lambda (t2: 
+T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u3: T).(\lambda (t2: 
+T).(eq T (THead k u2 t1) (THead k u3 t2)))) (\lambda (u3: T).(\lambda (_: 
+T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) v t1 
+t2)))) (ex_intro2 T (\lambda (u3: T).(eq T (THead k u2 t1) (THead k u3 t1))) 
+(\lambda (u3: T).(subst0 i v u1 u3)) u2 (refl_equal T (THead k u2 t1)) H19))) 
+t H12))) k0 H14)))))) H11)) H10)) x H4))))))))))))))))) (\lambda (H0: (subst0 
+i v (THead k u1 t1) x)).(\lambda (k0: K).(\lambda (v0: T).(\lambda (t0: 
+T).(\lambda (t3: T).(\lambda (i0: nat).(\lambda (u: T).(\lambda (H1: (eq nat 
+i0 i)).(\lambda (H2: (eq T v0 v)).(\lambda (H3: (eq T (THead k0 u t3) (THead 
+k u1 t1))).(\lambda (H4: (eq T (THead k0 u t0) x)).(\lambda (H5: (subst0 (s 
+k0 i0) v0 t3 t0)).(let H6 \def (eq_ind nat i0 (\lambda (n: nat).(subst0 (s k0 
+n) v0 t3 t0)) H5 i H1) in (let H7 \def (eq_ind T v0 (\lambda (t: T).(subst0 
+(s k0 i) t t3 t0)) H6 v H2) in (let H8 \def (eq_ind_r T x (\lambda (t: 
+T).(subst0 i v (THead k u1 t1) t)) H0 (THead k0 u t0) H4) in (let H9 \def 
+(eq_ind_r T x (\lambda (t: T).(subst0 i v (THead k u1 t1) t)) H (THead k0 u 
+t0) H4) in (eq_ind T (THead k0 u t0) (\lambda (t: T).(or3 (ex2 T (\lambda 
+(u2: T).(eq T t (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))) (ex2 
+T (\lambda (t2: T).(eq T t (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) 
+v t1 t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t (THead k u2 
+t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))) (let H10 \def (f_equal T K 
+(\lambda (e: T).(match e in T return (\lambda (_: T).K) with [(TSort _) 
+\Rightarrow k0 | (TLRef _) \Rightarrow k0 | (THead k1 _ _) \Rightarrow k1])) 
+(THead k0 u t3) (THead k u1 t1) H3) in ((let H11 \def (f_equal T T (\lambda 
+(e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u 
+| (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) (THead k0 u t3) 
+(THead k u1 t1) H3) in ((let H12 \def (f_equal T T (\lambda (e: T).(match e 
+in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t3 | (TLRef _) 
+\Rightarrow t3 | (THead _ _ t) \Rightarrow t])) (THead k0 u t3) (THead k u1 
+t1) H3) in (\lambda (H13: (eq T u u1)).(\lambda (H14: (eq K k0 k)).(let H15 
+\def (eq_ind T u (\lambda (t: T).(subst0 i v (THead k u1 t1) (THead k0 t 
+t0))) H9 u1 H13) in (let H16 \def (eq_ind T u (\lambda (t: T).(subst0 i v 
+(THead k u1 t1) (THead k0 t t0))) H8 u1 H13) in (eq_ind_r T u1 (\lambda (t: 
+T).(or3 (ex2 T (\lambda (u2: T).(eq T (THead k0 t t0) (THead k u2 t1))) 
+(\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t2: T).(eq T (THead k0 
+t t0) (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T 
+T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k0 t t0) (THead k u2 t2)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))) (let H17 \def (eq_ind T t3 
+(\lambda (t: T).(subst0 (s k0 i) v t t0)) H7 t1 H12) in (let H18 \def (eq_ind 
+K k0 (\lambda (k1: K).(subst0 i v (THead k u1 t1) (THead k1 u1 t0))) H15 k 
+H14) in (let H19 \def (eq_ind K k0 (\lambda (k1: K).(subst0 i v (THead k u1 
+t1) (THead k1 u1 t0))) H16 k H14) in (let H20 \def (eq_ind K k0 (\lambda (k1: 
+K).(subst0 (s k1 i) v t1 t0)) H17 k H14) in (eq_ind_r K k (\lambda (k1: 
+K).(or3 (ex2 T (\lambda (u2: T).(eq T (THead k1 u1 t0) (THead k u2 t1))) 
+(\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t2: T).(eq T (THead k1 
+u1 t0) (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T 
+T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k1 u1 t0) (THead k u2 t2)))) 
 (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: 
-T).(\lambda (t3: T).(subst0 (s k i) v t1 t3))))))) (\lambda (H13: (subst0 (s 
-k i) v t1 t2)).(or3_intro1 (ex2 T (\lambda (u2: T).(eq T (THead k u1 t2) 
-(THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))) (ex2 T (\lambda (t3: 
-T).(eq T (THead k u1 t2) (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v 
-t1 t3))) (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead k u1 t2) 
-(THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 u2))) 
-(\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))) (ex_intro2 T 
-(\lambda (t3: T).(eq T (THead k u1 t2) (THead k u1 t3))) (\lambda (t3: 
-T).(subst0 (s k i) v t1 t3)) t2 (refl_equal T (THead k u1 t2)) H13))) x H12)) 
-t0 (sym_eq T t0 t1 H11))) u (sym_eq T u u1 H10))) k0 (sym_eq K k0 k H9))) 
-H8)) H7))) v0 (sym_eq T v0 v H5))) i0 (sym_eq nat i0 i H1) H2 H3 H4 H0))))) | 
-(subst0_both v0 u0 u2 i0 H0 k0 t0 t2 H1) \Rightarrow (\lambda (H2: (eq nat i0 
-i)).(\lambda (H3: (eq T v0 v)).(\lambda (H4: (eq T (THead k0 u0 t0) (THead k 
-u1 t1))).(\lambda (H5: (eq T (THead k0 u2 t2) x)).(eq_ind nat i (\lambda (n: 
-nat).((eq T v0 v) \to ((eq T (THead k0 u0 t0) (THead k u1 t1)) \to ((eq T 
-(THead k0 u2 t2) x) \to ((subst0 n v0 u0 u2) \to ((subst0 (s k0 n) v0 t0 t2) 
-\to (or3 (ex2 T (\lambda (u3: T).(eq T x (THead k u3 t1))) (\lambda (u3: 
-T).(subst0 i v u1 u3))) (ex2 T (\lambda (t3: T).(eq T x (THead k u1 t3))) 
-(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u3: 
-T).(\lambda (t3: T).(eq T x (THead k u3 t3)))) (\lambda (u3: T).(\lambda (_: 
-T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 
-t3))))))))))) (\lambda (H6: (eq T v0 v)).(eq_ind T v (\lambda (t: T).((eq T 
-(THead k0 u0 t0) (THead k u1 t1)) \to ((eq T (THead k0 u2 t2) x) \to ((subst0 
-i t u0 u2) \to ((subst0 (s k0 i) t t0 t2) \to (or3 (ex2 T (\lambda (u3: 
-T).(eq T x (THead k u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T 
-(\lambda (t3: T).(eq T x (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v 
-t1 t3))) (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T x (THead k u3 
-t3)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
-T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))))))))) (\lambda (H7: (eq T 
-(THead k0 u0 t0) (THead k u1 t1))).(let H8 \def (f_equal T T (\lambda (e: 
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | 
-(TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k0 u0 t0) 
-(THead k u1 t1) H7) in ((let H9 \def (f_equal T T (\lambda (e: T).(match e in 
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) 
-\Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k0 u0 t0) (THead k u1 
-t1) H7) in ((let H10 \def (f_equal T K (\lambda (e: T).(match e in T return 
+T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))) (or3_intro1 (ex2 T (\lambda 
+(u2: T).(eq T (THead k u1 t0) (THead k u2 t1))) (\lambda (u2: T).(subst0 i v 
+u1 u2))) (ex2 T (\lambda (t2: T).(eq T (THead k u1 t0) (THead k u1 t2))) 
+(\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u2: 
+T).(\lambda (t2: T).(eq T (THead k u1 t0) (THead k u2 t2)))) (\lambda (u2: 
+T).(\lambda (_: T).(subst0 i v u1 u2))) (\lambda (_: T).(\lambda (t2: 
+T).(subst0 (s k i) v t1 t2)))) (ex_intro2 T (\lambda (t2: T).(eq T (THead k 
+u1 t0) (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2)) t0 
+(refl_equal T (THead k u1 t0)) H20)) k0 H14))))) u H13)))))) H11)) H10)) x 
+H4))))))))))))))))) (\lambda (H0: (subst0 i v (THead k u1 t1) x)).(\lambda 
+(v0: T).(\lambda (u0: T).(\lambda (u2: T).(\lambda (i0: nat).(\lambda (k0: 
+K).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H2: (eq nat i0 i)).(\lambda 
+(H3: (eq T v0 v)).(\lambda (H4: (eq T (THead k0 u0 t0) (THead k u1 
+t1))).(\lambda (H5: (eq T (THead k0 u2 t3) x)).(\lambda (H1: (subst0 i0 v0 u0 
+u2)).(\lambda (H6: (subst0 (s k0 i0) v0 t0 t3)).(let H7 \def (eq_ind nat i0 
+(\lambda (n: nat).(subst0 (s k0 n) v0 t0 t3)) H6 i H2) in (let H8 \def 
+(eq_ind nat i0 (\lambda (n: nat).(subst0 n v0 u0 u2)) H1 i H2) in (let H9 
+\def (eq_ind T v0 (\lambda (t: T).(subst0 (s k0 i) t t0 t3)) H7 v H3) in (let 
+H10 \def (eq_ind T v0 (\lambda (t: T).(subst0 i t u0 u2)) H8 v H3) in (let 
+H11 \def (eq_ind_r T x (\lambda (t: T).(subst0 i v (THead k u1 t1) t)) H0 
+(THead k0 u2 t3) H5) in (let H12 \def (eq_ind_r T x (\lambda (t: T).(subst0 i 
+v (THead k u1 t1) t)) H (THead k0 u2 t3) H5) in (eq_ind T (THead k0 u2 t3) 
+(\lambda (t: T).(or3 (ex2 T (\lambda (u3: T).(eq T t (THead k u3 t1))) 
+(\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq T t (THead 
+k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda 
+(u3: T).(\lambda (t2: T).(eq T t (THead k u3 t2)))) (\lambda (u3: T).(\lambda 
+(_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) 
+v t1 t2)))))) (let H13 \def (f_equal T K (\lambda (e: T).(match e in T return 
 (\lambda (_: T).K) with [(TSort _) \Rightarrow k0 | (TLRef _) \Rightarrow k0 
-| (THead k1 _ _) \Rightarrow k1])) (THead k0 u0 t0) (THead k u1 t1) H7) in 
-(eq_ind K k (\lambda (k1: K).((eq T u0 u1) \to ((eq T t0 t1) \to ((eq T 
-(THead k1 u2 t2) x) \to ((subst0 i v u0 u2) \to ((subst0 (s k1 i) v t0 t2) 
-\to (or3 (ex2 T (\lambda (u3: T).(eq T x (THead k u3 t1))) (\lambda (u3: 
-T).(subst0 i v u1 u3))) (ex2 T (\lambda (t3: T).(eq T x (THead k u1 t3))) 
-(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u3: 
-T).(\lambda (t3: T).(eq T x (THead k u3 t3)))) (\lambda (u3: T).(\lambda (_: 
-T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 
-t3))))))))))) (\lambda (H11: (eq T u0 u1)).(eq_ind T u1 (\lambda (t: T).((eq 
-T t0 t1) \to ((eq T (THead k u2 t2) x) \to ((subst0 i v t u2) \to ((subst0 (s 
-k i) v t0 t2) \to (or3 (ex2 T (\lambda (u3: T).(eq T x (THead k u3 t1))) 
-(\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t3: T).(eq T x (THead 
-k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda 
-(u3: T).(\lambda (t3: T).(eq T x (THead k u3 t3)))) (\lambda (u3: T).(\lambda 
-(_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) 
-v t1 t3)))))))))) (\lambda (H12: (eq T t0 t1)).(eq_ind T t1 (\lambda (t: 
-T).((eq T (THead k u2 t2) x) \to ((subst0 i v u1 u2) \to ((subst0 (s k i) v t 
-t2) \to (or3 (ex2 T (\lambda (u3: T).(eq T x (THead k u3 t1))) (\lambda (u3: 
-T).(subst0 i v u1 u3))) (ex2 T (\lambda (t3: T).(eq T x (THead k u1 t3))) 
-(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u3: 
-T).(\lambda (t3: T).(eq T x (THead k u3 t3)))) (\lambda (u3: T).(\lambda (_: 
-T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 
-t3))))))))) (\lambda (H13: (eq T (THead k u2 t2) x)).(eq_ind T (THead k u2 
-t2) (\lambda (t: T).((subst0 i v u1 u2) \to ((subst0 (s k i) v t1 t2) \to 
-(or3 (ex2 T (\lambda (u3: T).(eq T t (THead k u3 t1))) (\lambda (u3: 
-T).(subst0 i v u1 u3))) (ex2 T (\lambda (t3: T).(eq T t (THead k u1 t3))) 
-(\lambda (t3: T).(subst0 (s k i) v t1 t3))) (ex3_2 T T (\lambda (u3: 
-T).(\lambda (t3: T).(eq T t (THead k u3 t3)))) (\lambda (u3: T).(\lambda (_: 
-T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i) v t1 
-t3)))))))) (\lambda (H14: (subst0 i v u1 u2)).(\lambda (H15: (subst0 (s k i) 
-v t1 t2)).(or3_intro2 (ex2 T (\lambda (u3: T).(eq T (THead k u2 t2) (THead k 
-u3 t1))) (\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t3: T).(eq T 
-(THead k u2 t2) (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1 t3))) 
-(ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead k u2 t2) (THead k 
-u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
-T).(\lambda (t3: T).(subst0 (s k i) v t1 t3)))) (ex3_2_intro T T (\lambda 
-(u3: T).(\lambda (t3: T).(eq T (THead k u2 t2) (THead k u3 t3)))) (\lambda 
-(u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t3: 
-T).(subst0 (s k i) v t1 t3))) u2 t2 (refl_equal T (THead k u2 t2)) H14 
-H15)))) x H13)) t0 (sym_eq T t0 t1 H12))) u0 (sym_eq T u0 u1 H11))) k0 
-(sym_eq K k0 k H10))) H9)) H8))) v0 (sym_eq T v0 v H6))) i0 (sym_eq nat i0 i 
-H2) H3 H4 H5 H0 H1)))))]) in (H0 (refl_equal nat i) (refl_equal T v) 
-(refl_equal T (THead k u1 t1)) (refl_equal T x))))))))).
+| (THead k1 _ _) \Rightarrow k1])) (THead k0 u0 t0) (THead k u1 t1) H4) in 
+((let H14 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: 
+T).T) with [(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t 
+_) \Rightarrow t])) (THead k0 u0 t0) (THead k u1 t1) H4) in ((let H15 \def 
+(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
+[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) 
+\Rightarrow t])) (THead k0 u0 t0) (THead k u1 t1) H4) in (\lambda (H16: (eq T 
+u0 u1)).(\lambda (H17: (eq K k0 k)).(let H18 \def (eq_ind T t0 (\lambda (t: 
+T).(subst0 (s k0 i) v t t3)) H9 t1 H15) in (let H19 \def (eq_ind K k0 
+(\lambda (k1: K).(subst0 i v (THead k u1 t1) (THead k1 u2 t3))) H12 k H17) in 
+(let H20 \def (eq_ind K k0 (\lambda (k1: K).(subst0 i v (THead k u1 t1) 
+(THead k1 u2 t3))) H11 k H17) in (let H21 \def (eq_ind K k0 (\lambda (k1: 
+K).(subst0 (s k1 i) v t1 t3)) H18 k H17) in (eq_ind_r K k (\lambda (k1: 
+K).(or3 (ex2 T (\lambda (u3: T).(eq T (THead k1 u2 t3) (THead k u3 t1))) 
+(\lambda (u3: T).(subst0 i v u1 u3))) (ex2 T (\lambda (t2: T).(eq T (THead k1 
+u2 t3) (THead k u1 t2))) (\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T 
+T (\lambda (u3: T).(\lambda (t2: T).(eq T (THead k1 u2 t3) (THead k u3 t2)))) 
+(\lambda (u3: T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s k i) v t1 t2)))))) (let H22 \def (eq_ind T u0 
+(\lambda (t: T).(subst0 i v t u2)) H10 u1 H16) in (or3_intro2 (ex2 T (\lambda 
+(u3: T).(eq T (THead k u2 t3) (THead k u3 t1))) (\lambda (u3: T).(subst0 i v 
+u1 u3))) (ex2 T (\lambda (t2: T).(eq T (THead k u2 t3) (THead k u1 t2))) 
+(\lambda (t2: T).(subst0 (s k i) v t1 t2))) (ex3_2 T T (\lambda (u3: 
+T).(\lambda (t2: T).(eq T (THead k u2 t3) (THead k u3 t2)))) (\lambda (u3: 
+T).(\lambda (_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: 
+T).(subst0 (s k i) v t1 t2)))) (ex3_2_intro T T (\lambda (u3: T).(\lambda 
+(t2: T).(eq T (THead k u2 t3) (THead k u3 t2)))) (\lambda (u3: T).(\lambda 
+(_: T).(subst0 i v u1 u3))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k i) 
+v t1 t2))) u2 t3 (refl_equal T (THead k u2 t3)) H22 H21))) k0 H17)))))))) 
+H14)) H13)) x H5))))))))))))))))))))) H))))))).
 
 theorem subst0_gen_lift_lt:
  \forall (u: T).(\forall (t1: T).(\forall (x: T).(\forall (i: nat).(\forall