-u1) (subst i v0 u2))).(\lambda (t: T).(\lambda (k: K).(let TMP_50 \def (subst
-i v0 u1) in (let TMP_51 \def (s k i) in (let TMP_52 \def (subst TMP_51 v0 t)
-in (let TMP_53 \def (THead k TMP_50 TMP_52) in (let TMP_56 \def (\lambda (t0:
-T).(let TMP_54 \def (THead k u2 t) in (let TMP_55 \def (subst i v0 TMP_54) in
-(eq T t0 TMP_55)))) in (let TMP_57 \def (subst i v0 u2) in (let TMP_58 \def
-(s k i) in (let TMP_59 \def (subst TMP_58 v0 t) in (let TMP_60 \def (THead k
-TMP_57 TMP_59) in (let TMP_65 \def (\lambda (t0: T).(let TMP_61 \def (subst i
-v0 u1) in (let TMP_62 \def (s k i) in (let TMP_63 \def (subst TMP_62 v0 t) in
-(let TMP_64 \def (THead k TMP_61 TMP_63) in (eq T TMP_64 t0)))))) in (let
-TMP_66 \def (subst i v0 u2) in (let TMP_74 \def (\lambda (t0: T).(let TMP_67
-\def (s k i) in (let TMP_68 \def (subst TMP_67 v0 t) in (let TMP_69 \def
-(THead k t0 TMP_68) in (let TMP_70 \def (subst i v0 u2) in (let TMP_71 \def
-(s k i) in (let TMP_72 \def (subst TMP_71 v0 t) in (let TMP_73 \def (THead k
-TMP_70 TMP_72) in (eq T TMP_69 TMP_73))))))))) in (let TMP_75 \def (subst i
-v0 u2) in (let TMP_76 \def (s k i) in (let TMP_77 \def (subst TMP_76 v0 t) in
-(let TMP_78 \def (THead k TMP_75 TMP_77) in (let TMP_79 \def (refl_equal T
-TMP_78) in (let TMP_80 \def (subst i v0 u1) in (let TMP_81 \def (eq_ind_r T
-TMP_66 TMP_74 TMP_79 TMP_80 H1) in (let TMP_82 \def (THead k u2 t) in (let
-TMP_83 \def (subst i v0 TMP_82) in (let TMP_84 \def (subst_head k v0 u2 t i)
-in (let TMP_85 \def (eq_ind_r T TMP_60 TMP_65 TMP_81 TMP_83 TMP_84) in (let
-TMP_86 \def (THead k u1 t) in (let TMP_87 \def (subst i v0 TMP_86) in (let
-TMP_88 \def (subst_head k v0 u1 t i) in (eq_ind_r T TMP_53 TMP_56 TMP_85
-TMP_87 TMP_88))))))))))))))))))))))))))))))))))) in (let TMP_130 \def
-(\lambda (k: K).(\lambda (v0: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda
-(i: nat).(\lambda (_: (subst0 (s k i) v0 t4 t3)).(\lambda (H1: (eq T (subst
-(s k i) v0 t4) (subst (s k i) v0 t3))).(\lambda (u: T).(let TMP_90 \def
-(subst i v0 u) in (let TMP_91 \def (s k i) in (let TMP_92 \def (subst TMP_91
-v0 t4) in (let TMP_93 \def (THead k TMP_90 TMP_92) in (let TMP_96 \def
-(\lambda (t: T).(let TMP_94 \def (THead k u t3) in (let TMP_95 \def (subst i
-v0 TMP_94) in (eq T t TMP_95)))) in (let TMP_97 \def (subst i v0 u) in (let
-TMP_98 \def (s k i) in (let TMP_99 \def (subst TMP_98 v0 t3) in (let TMP_100
-\def (THead k TMP_97 TMP_99) in (let TMP_105 \def (\lambda (t: T).(let
-TMP_101 \def (subst i v0 u) in (let TMP_102 \def (s k i) in (let TMP_103 \def
-(subst TMP_102 v0 t4) in (let TMP_104 \def (THead k TMP_101 TMP_103) in (eq T
-TMP_104 t)))))) in (let TMP_106 \def (s k i) in (let TMP_107 \def (subst
-TMP_106 v0 t3) in (let TMP_114 \def (\lambda (t: T).(let TMP_108 \def (subst
-i v0 u) in (let TMP_109 \def (THead k TMP_108 t) in (let TMP_110 \def (subst
-i v0 u) in (let TMP_111 \def (s k i) in (let TMP_112 \def (subst TMP_111 v0
-t3) in (let TMP_113 \def (THead k TMP_110 TMP_112) in (eq T TMP_109
-TMP_113)))))))) in (let TMP_115 \def (subst i v0 u) in (let TMP_116 \def (s k
-i) in (let TMP_117 \def (subst TMP_116 v0 t3) in (let TMP_118 \def (THead k
-TMP_115 TMP_117) in (let TMP_119 \def (refl_equal T TMP_118) in (let TMP_120
-\def (s k i) in (let TMP_121 \def (subst TMP_120 v0 t4) in (let TMP_122 \def
-(eq_ind_r T TMP_107 TMP_114 TMP_119 TMP_121 H1) in (let TMP_123 \def (THead k
-u t3) in (let TMP_124 \def (subst i v0 TMP_123) in (let TMP_125 \def
-(subst_head k v0 u t3 i) in (let TMP_126 \def (eq_ind_r T TMP_100 TMP_105
-TMP_122 TMP_124 TMP_125) in (let TMP_127 \def (THead k u t4) in (let TMP_128
-\def (subst i v0 TMP_127) in (let TMP_129 \def (subst_head k v0 u t4 i) in
-(eq_ind_r T TMP_93 TMP_96 TMP_126 TMP_128
-TMP_129))))))))))))))))))))))))))))))))))))) in (let TMP_182 \def (\lambda
-(v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda (_:
-(subst0 i v0 u1 u2)).(\lambda (H1: (eq T (subst i v0 u1) (subst i v0
-u2))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (subst0
-(s k i) v0 t3 t4)).(\lambda (H3: (eq T (subst (s k i) v0 t3) (subst (s k i)
-v0 t4))).(let TMP_131 \def (subst i v0 u1) in (let TMP_132 \def (s k i) in
-(let TMP_133 \def (subst TMP_132 v0 t3) in (let TMP_134 \def (THead k TMP_131
-TMP_133) in (let TMP_137 \def (\lambda (t: T).(let TMP_135 \def (THead k u2
-t4) in (let TMP_136 \def (subst i v0 TMP_135) in (eq T t TMP_136)))) in (let
-TMP_138 \def (subst i v0 u2) in (let TMP_139 \def (s k i) in (let TMP_140
-\def (subst TMP_139 v0 t4) in (let TMP_141 \def (THead k TMP_138 TMP_140) in
-(let TMP_146 \def (\lambda (t: T).(let TMP_142 \def (subst i v0 u1) in (let
-TMP_143 \def (s k i) in (let TMP_144 \def (subst TMP_143 v0 t3) in (let
-TMP_145 \def (THead k TMP_142 TMP_144) in (eq T TMP_145 t)))))) in (let
-TMP_147 \def (subst i v0 u2) in (let TMP_155 \def (\lambda (t: T).(let
-TMP_148 \def (s k i) in (let TMP_149 \def (subst TMP_148 v0 t3) in (let
-TMP_150 \def (THead k t TMP_149) in (let TMP_151 \def (subst i v0 u2) in (let
-TMP_152 \def (s k i) in (let TMP_153 \def (subst TMP_152 v0 t4) in (let
-TMP_154 \def (THead k TMP_151 TMP_153) in (eq T TMP_150 TMP_154))))))))) in
-(let TMP_156 \def (s k i) in (let TMP_157 \def (subst TMP_156 v0 t4) in (let
-TMP_164 \def (\lambda (t: T).(let TMP_158 \def (subst i v0 u2) in (let
-TMP_159 \def (THead k TMP_158 t) in (let TMP_160 \def (subst i v0 u2) in (let
-TMP_161 \def (s k i) in (let TMP_162 \def (subst TMP_161 v0 t4) in (let
-TMP_163 \def (THead k TMP_160 TMP_162) in (eq T TMP_159 TMP_163)))))))) in
-(let TMP_165 \def (subst i v0 u2) in (let TMP_166 \def (s k i) in (let
-TMP_167 \def (subst TMP_166 v0 t4) in (let TMP_168 \def (THead k TMP_165
-TMP_167) in (let TMP_169 \def (refl_equal T TMP_168) in (let TMP_170 \def (s
-k i) in (let TMP_171 \def (subst TMP_170 v0 t3) in (let TMP_172 \def
-(eq_ind_r T TMP_157 TMP_164 TMP_169 TMP_171 H3) in (let TMP_173 \def (subst i
-v0 u1) in (let TMP_174 \def (eq_ind_r T TMP_147 TMP_155 TMP_172 TMP_173 H1)
-in (let TMP_175 \def (THead k u2 t4) in (let TMP_176 \def (subst i v0
-TMP_175) in (let TMP_177 \def (subst_head k v0 u2 t4 i) in (let TMP_178 \def
-(eq_ind_r T TMP_141 TMP_146 TMP_174 TMP_176 TMP_177) in (let TMP_179 \def
-(THead k u1 t3) in (let TMP_180 \def (subst i v0 TMP_179) in (let TMP_181
-\def (subst_head k v0 u1 t3 i) in (eq_ind_r T TMP_134 TMP_137 TMP_178 TMP_180
-TMP_181)))))))))))))))))))))))))))))))))))))))))))) in (subst0_ind TMP_3
-TMP_49 TMP_89 TMP_130 TMP_182 d v t1 t2 H)))))))))).