-t) (THead k u2 t)) (subst0_fst v x u2 i0 H6 t k))) (\lambda (H6: (subst0 i0 v
-x u2)).(or4_intro3 (eq T (THead k u2 t) (THead k x t)) (ex2 T (\lambda (t3:
-T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k x
-t) t3))) (subst0 i0 v (THead k u2 t) (THead k x t)) (subst0 i0 v (THead k x
-t) (THead k u2 t)) (subst0_fst v u2 x i0 H6 t k))) (H1 x H5)) t2 H4)))) H3))
-(\lambda (H3: (ex2 T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda
-(t2: T).(subst0 (s k i0) v t t2)))).(ex2_ind T (\lambda (t3: T).(eq T t2
-(THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i0) v t t3)) (or4 (eq T
-(THead k u2 t) t2) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
-(\lambda (t3: T).(subst0 i0 v t2 t3))) (subst0 i0 v (THead k u2 t) t2)
-(subst0 i0 v t2 (THead k u2 t))) (\lambda (x: T).(\lambda (H4: (eq T t2
-(THead k u1 x))).(\lambda (H5: (subst0 (s k i0) v t x)).(eq_ind_r T (THead k
-u1 x) (\lambda (t3: T).(or4 (eq T (THead k u2 t) t3) (ex2 T (\lambda (t4:
-T).(subst0 i0 v (THead k u2 t) t4)) (\lambda (t4: T).(subst0 i0 v t3 t4)))
-(subst0 i0 v (THead k u2 t) t3) (subst0 i0 v t3 (THead k u2 t)))) (or4_ind
-(eq T u2 u2) (ex2 T (\lambda (t3: T).(subst0 i0 v u2 t3)) (\lambda (t3:
-T).(subst0 i0 v u2 t3))) (subst0 i0 v u2 u2) (subst0 i0 v u2 u2) (or4 (eq T
-(THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k
-u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v
-(THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t)))
-(\lambda (_: (eq T u2 u2)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x))
+t) (THead k u2 t)) (ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t)
+t3)) (\lambda (t3: T).(subst0 i0 v (THead k x t) t3)) (THead k x0 t)
+(subst0_fst v x0 u2 i0 H7 t k) (subst0_fst v x0 x i0 H8 t k)))))) H6))
+(\lambda (H6: (subst0 i0 v u2 x)).(or4_intro2 (eq T (THead k u2 t) (THead k x
+t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
+T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t) (THead k x
+t)) (subst0 i0 v (THead k x t) (THead k u2 t)) (subst0_fst v x u2 i0 H6 t
+k))) (\lambda (H6: (subst0 i0 v x u2)).(or4_intro3 (eq T (THead k u2 t)
+(THead k x t)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3))
+(\lambda (t3: T).(subst0 i0 v (THead k x t) t3))) (subst0 i0 v (THead k u2 t)
+(THead k x t)) (subst0 i0 v (THead k x t) (THead k u2 t)) (subst0_fst v u2 x
+i0 H6 t k))) (H1 x H5)) t2 H4)))) H3)) (\lambda (H3: (ex2 T (\lambda (t3:
+T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i0) v t
+t3)))).(ex2_ind T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda (t3:
+T).(subst0 (s k i0) v t t3)) (or4 (eq T (THead k u2 t) t2) (ex2 T (\lambda
+(t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v t2
+t3))) (subst0 i0 v (THead k u2 t) t2) (subst0 i0 v t2 (THead k u2 t)))
+(\lambda (x: T).(\lambda (H4: (eq T t2 (THead k u1 x))).(\lambda (H5: (subst0
+(s k i0) v t x)).(eq_ind_r T (THead k u1 x) (\lambda (t3: T).(or4 (eq T
+(THead k u2 t) t3) (ex2 T (\lambda (t4: T).(subst0 i0 v (THead k u2 t) t4))
+(\lambda (t4: T).(subst0 i0 v t3 t4))) (subst0 i0 v (THead k u2 t) t3)
+(subst0 i0 v t3 (THead k u2 t)))) (or4_ind (eq T u2 u2) (ex2 T (\lambda (t3:
+T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v u2 t3))) (subst0 i0 v
+u2 u2) (subst0 i0 v u2 u2) (or4 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T
+(\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0
+v (THead k u1 x) t3))) (subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0
+v (THead k u1 x) (THead k u2 t))) (\lambda (_: (eq T u2 u2)).(or4_intro1 (eq
+T (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0 v (THead
+k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3))) (subst0 i0 v
+(THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x) (THead k u2 t))
+(ex_intro2 T (\lambda (t3: T).(subst0 i0 v (THead k u2 t) t3)) (\lambda (t3:
+T).(subst0 i0 v (THead k u1 x) t3)) (THead k u2 x) (subst0_snd k v x t i0 H5
+u2) (subst0_fst v u2 u1 i0 H0 x k)))) (\lambda (H6: (ex2 T (\lambda (t3:
+T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v u2 t3)))).(ex2_ind T
+(\lambda (t3: T).(subst0 i0 v u2 t3)) (\lambda (t3: T).(subst0 i0 v u2 t3))
+(or4 (eq T (THead k u2 t) (THead k u1 x)) (ex2 T (\lambda (t3: T).(subst0 i0
+v (THead k u2 t) t3)) (\lambda (t3: T).(subst0 i0 v (THead k u1 x) t3)))
+(subst0 i0 v (THead k u2 t) (THead k u1 x)) (subst0 i0 v (THead k u1 x)
+(THead k u2 t))) (\lambda (x0: T).(\lambda (_: (subst0 i0 v u2 x0)).(\lambda
+(_: (subst0 i0 v u2 x0)).(or4_intro1 (eq T (THead k u2 t) (THead k u1 x))