+\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)).(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) 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))))) 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 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 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 (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) 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))))))).