-k x0 x1) t3)) (THead k x x1) (subst0_both u3 u2 x i2 H8 k t x1 H7)
-(subst0_fst v x x0 i H9 x1 k))))) (H1 x0 u3 i2 H6 H3)) t2 H5)))))) H4))
-(subst0_gen_head k u3 u0 t t2 i2 H2))))))))))))))) (\lambda (k: K).(\lambda
-(v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H0:
-(subst0 (s k i) v t3 t2)).(\lambda (H1: ((\forall (t4: T).(\forall (u2:
-T).(\forall (i2: nat).((subst0 i2 u2 t3 t4) \to ((not (eq nat (s k i) i2))
-\to (ex2 T (\lambda (t: T).(subst0 i2 u2 t2 t)) (\lambda (t: T).(subst0 (s k
-i) v t4 t)))))))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (u2:
-T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u2 (THead k u t3)
+k x t) t3)) (THead k x0 t) (subst0_fst u3 x0 u2 i2 H7 t k) (subst0_fst v x0 x
+i H8 t k))))) (H1 x u3 i2 H6 H3)) t2 H5)))) H4)) (\lambda (H4: (ex2 T
+(\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda (t3: T).(subst0 (s k i2)
+u3 t t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u0 t3))) (\lambda
+(t3: T).(subst0 (s k i2) u3 t t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3
+(THead k u2 t) t3)) (\lambda (t3: T).(subst0 i v t2 t3))) (\lambda (x:
+T).(\lambda (H5: (eq T t2 (THead k u0 x))).(\lambda (H6: (subst0 (s k i2) u3
+t x)).(eq_ind_r T (THead k u0 x) (\lambda (t3: T).(ex2 T (\lambda (t4:
+T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i v t3 t4))))
+(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3:
+T).(subst0 i v (THead k u0 x) t3)) (THead k u2 x) (subst0_snd k u3 x t i2 H6
+u2) (subst0_fst v u2 u0 i H0 x k)) t2 H5)))) H4)) (\lambda (H4: (ex3_2 T T
+(\lambda (u4: T).(\lambda (t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4:
+T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3:
+T).(subst0 (s k i2) u3 t t3))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda
+(t3: T).(eq T t2 (THead k u4 t3)))) (\lambda (u4: T).(\lambda (_: T).(subst0
+i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t3: T).(subst0 (s k i2) u3 t t3)))
+(ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda (t3:
+T).(subst0 i v t2 t3))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T
+t2 (THead k x0 x1))).(\lambda (H6: (subst0 i2 u3 u0 x0)).(\lambda (H7:
+(subst0 (s k i2) u3 t x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t3: T).(ex2
+T (\lambda (t4: T).(subst0 i2 u3 (THead k u2 t) t4)) (\lambda (t4: T).(subst0
+i v t3 t4)))) (ex2_ind T (\lambda (t3: T).(subst0 i2 u3 u2 t3)) (\lambda (t3:
+T).(subst0 i v x0 t3)) (ex2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t)
+t3)) (\lambda (t3: T).(subst0 i v (THead k x0 x1) t3))) (\lambda (x:
+T).(\lambda (H8: (subst0 i2 u3 u2 x)).(\lambda (H9: (subst0 i v x0
+x)).(ex_intro2 T (\lambda (t3: T).(subst0 i2 u3 (THead k u2 t) t3)) (\lambda
+(t3: T).(subst0 i v (THead k x0 x1) t3)) (THead k x x1) (subst0_both u3 u2 x
+i2 H8 k t x1 H7) (subst0_fst v x x0 i H9 x1 k))))) (H1 x0 u3 i2 H6 H3)) t2
+H5)))))) H4)) (subst0_gen_head k u3 u0 t t2 i2 H2))))))))))))))) (\lambda (k:
+K).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (i:
+nat).(\lambda (H0: (subst0 (s k i) v t3 t2)).(\lambda (H1: ((\forall (t4:
+T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t3 t4) \to ((not (eq
+nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u2 t2 t)) (\lambda (t:
+T).(subst0 (s k i) v t4 t)))))))))).(\lambda (u: T).(\lambda (t4: T).(\lambda
+(u2: T).(\lambda (i2: nat).(\lambda (H2: (subst0 i2 u2 (THead k u t3)