-(x: T).(\lambda (i: nat).(\lambda (H: (subst1 i v (THead k u1 t1)
-x)).(subst1_ind i v (THead k u1 t1) (\lambda (t: T).(ex3_2 T T (\lambda (u2:
-T).(\lambda (t2: T).(eq T t (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_:
-T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1
-t2))))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k u1
-t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2)))
-(\lambda (_: T).(\lambda (t2: T).(subst1 (s k i) v t1 t2))) u1 t1 (refl_equal
-T (THead k u1 t1)) (subst1_refl i v u1) (subst1_refl (s k i) v t1)) (\lambda
-(t2: T).(\lambda (H0: (subst0 i v (THead k u1 t1) t2)).(or3_ind (ex2 T
-(\lambda (u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1
-u2))) (ex2 T (\lambda (t3: T).(eq T 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 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)))) (ex3_2
-T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3)))) (\lambda
-(u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_: T).(\lambda (t3:
-T).(subst1 (s k i) v t1 t3)))) (\lambda (H1: (ex2 T (\lambda (u2: T).(eq T t2
-(THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2)))).(ex2_ind T (\lambda
-(u2: T).(eq T t2 (THead k u2 t1))) (\lambda (u2: T).(subst0 i v u1 u2))
-(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2 t3))))
-(\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
-T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0: T).(\lambda
-(H2: (eq T t2 (THead k x0 t1))).(\lambda (H3: (subst0 i v u1
-x0)).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead k u2
-t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) (\lambda (_:
-T).(\lambda (t3: T).(subst1 (s k i) v t1 t3))) x0 t1 H2 (subst1_single i v u1
-x0 H3) (subst1_refl (s k i) v t1))))) H1)) (\lambda (H1: (ex2 T (\lambda (t3:
-T).(eq T t2 (THead k u1 t3))) (\lambda (t3: T).(subst0 (s k i) v t1
-t3)))).(ex2_ind T (\lambda (t3: T).(eq T 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 t2 (THead k u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2)))
-(\lambda (_: T).(\lambda (t3: T).(subst1 (s k i) v t1 t3)))) (\lambda (x0:
+(x: T).(\lambda (i: nat).(\lambda (H: (subst1 i v (THead k u1 t1) x)).(let
+TMP_1 \def (THead k u1 t1) in (let TMP_7 \def (\lambda (t: T).(let TMP_3 \def
+(\lambda (u2: T).(\lambda (t2: T).(let TMP_2 \def (THead k u2 t2) in (eq T t
+TMP_2)))) in (let TMP_4 \def (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1
+u2))) in (let TMP_6 \def (\lambda (_: T).(\lambda (t2: T).(let TMP_5 \def (s
+k i) in (subst1 TMP_5 v t1 t2)))) in (ex3_2 T T TMP_3 TMP_4 TMP_6))))) in
+(let TMP_10 \def (\lambda (u2: T).(\lambda (t2: T).(let TMP_8 \def (THead k
+u1 t1) in (let TMP_9 \def (THead k u2 t2) in (eq T TMP_8 TMP_9))))) in (let
+TMP_11 \def (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) in (let
+TMP_13 \def (\lambda (_: T).(\lambda (t2: T).(let TMP_12 \def (s k i) in
+(subst1 TMP_12 v t1 t2)))) in (let TMP_14 \def (THead k u1 t1) in (let TMP_15
+\def (refl_equal T TMP_14) in (let TMP_16 \def (subst1_refl i v u1) in (let
+TMP_17 \def (s k i) in (let TMP_18 \def (subst1_refl TMP_17 v t1) in (let
+TMP_19 \def (ex3_2_intro T T TMP_10 TMP_11 TMP_13 u1 t1 TMP_15 TMP_16 TMP_18)
+in (let TMP_102 \def (\lambda (t2: T).(\lambda (H0: (subst0 i v (THead k u1
+t1) t2)).(let TMP_21 \def (\lambda (u2: T).(let TMP_20 \def (THead k u2 t1)
+in (eq T t2 TMP_20))) in (let TMP_22 \def (\lambda (u2: T).(subst0 i v u1
+u2)) in (let TMP_23 \def (ex2 T TMP_21 TMP_22) in (let TMP_25 \def (\lambda
+(t3: T).(let TMP_24 \def (THead k u1 t3) in (eq T t2 TMP_24))) in (let TMP_27
+\def (\lambda (t3: T).(let TMP_26 \def (s k i) in (subst0 TMP_26 v t1 t3)))
+in (let TMP_28 \def (ex2 T TMP_25 TMP_27) in (let TMP_30 \def (\lambda (u2:
+T).(\lambda (t3: T).(let TMP_29 \def (THead k u2 t3) in (eq T t2 TMP_29))))
+in (let TMP_31 \def (\lambda (u2: T).(\lambda (_: T).(subst0 i v u1 u2))) in
+(let TMP_33 \def (\lambda (_: T).(\lambda (t3: T).(let TMP_32 \def (s k i) in
+(subst0 TMP_32 v t1 t3)))) in (let TMP_34 \def (ex3_2 T T TMP_30 TMP_31
+TMP_33) in (let TMP_36 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_35
+\def (THead k u2 t3) in (eq T t2 TMP_35)))) in (let TMP_37 \def (\lambda (u2:
+T).(\lambda (_: T).(subst1 i v u1 u2))) in (let TMP_39 \def (\lambda (_:
+T).(\lambda (t3: T).(let TMP_38 \def (s k i) in (subst1 TMP_38 v t1 t3)))) in
+(let TMP_40 \def (ex3_2 T T TMP_36 TMP_37 TMP_39) in (let TMP_59 \def
+(\lambda (H1: (ex2 T (\lambda (u2: T).(eq T t2 (THead k u2 t1))) (\lambda
+(u2: T).(subst0 i v u1 u2)))).(let TMP_42 \def (\lambda (u2: T).(let TMP_41
+\def (THead k u2 t1) in (eq T t2 TMP_41))) in (let TMP_43 \def (\lambda (u2:
+T).(subst0 i v u1 u2)) in (let TMP_45 \def (\lambda (u2: T).(\lambda (t3:
+T).(let TMP_44 \def (THead k u2 t3) in (eq T t2 TMP_44)))) in (let TMP_46
+\def (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) in (let TMP_48
+\def (\lambda (_: T).(\lambda (t3: T).(let TMP_47 \def (s k i) in (subst1
+TMP_47 v t1 t3)))) in (let TMP_49 \def (ex3_2 T T TMP_45 TMP_46 TMP_48) in
+(let TMP_58 \def (\lambda (x0: T).(\lambda (H2: (eq T t2 (THead k x0
+t1))).(\lambda (H3: (subst0 i v u1 x0)).(let TMP_51 \def (\lambda (u2:
+T).(\lambda (t3: T).(let TMP_50 \def (THead k u2 t3) in (eq T t2 TMP_50))))
+in (let TMP_52 \def (\lambda (u2: T).(\lambda (_: T).(subst1 i v u1 u2))) in
+(let TMP_54 \def (\lambda (_: T).(\lambda (t3: T).(let TMP_53 \def (s k i) in
+(subst1 TMP_53 v t1 t3)))) in (let TMP_55 \def (subst1_single i v u1 x0 H3)
+in (let TMP_56 \def (s k i) in (let TMP_57 \def (subst1_refl TMP_56 v t1) in
+(ex3_2_intro T T TMP_51 TMP_52 TMP_54 x0 t1 H2 TMP_55 TMP_57)))))))))) in
+(ex2_ind T TMP_42 TMP_43 TMP_49 TMP_58 H1))))))))) in (let TMP_79 \def
+(\lambda (H1: (ex2 T (\lambda (t3: T).(eq T t2 (THead k u1 t3))) (\lambda
+(t3: T).(subst0 (s k i) v t1 t3)))).(let TMP_61 \def (\lambda (t3: T).(let
+TMP_60 \def (THead k u1 t3) in (eq T t2 TMP_60))) in (let TMP_63 \def
+(\lambda (t3: T).(let TMP_62 \def (s k i) in (subst0 TMP_62 v t1 t3))) in
+(let TMP_65 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_64 \def (THead k
+u2 t3) in (eq T t2 TMP_64)))) in (let TMP_66 \def (\lambda (u2: T).(\lambda
+(_: T).(subst1 i v u1 u2))) in (let TMP_68 \def (\lambda (_: T).(\lambda (t3:
+T).(let TMP_67 \def (s k i) in (subst1 TMP_67 v t1 t3)))) in (let TMP_69 \def
+(ex3_2 T T TMP_65 TMP_66 TMP_68) in (let TMP_78 \def (\lambda (x0: