-(lift h d t4)))))).(\lambda (h: nat).(\lambda (d: nat).(let TMP_40 \def (Flat
-Appl) in (let TMP_41 \def (lift h d v1) in (let TMP_42 \def (Flat Appl) in
-(let TMP_43 \def (s TMP_42 d) in (let TMP_44 \def (Bind Abst) in (let TMP_45
-\def (THead TMP_44 u t3) in (let TMP_46 \def (lift h TMP_43 TMP_45) in (let
-TMP_47 \def (THead TMP_40 TMP_41 TMP_46) in (let TMP_51 \def (\lambda (t:
-T).(let TMP_48 \def (Bind Abbr) in (let TMP_49 \def (THead TMP_48 v2 t4) in
-(let TMP_50 \def (lift h d TMP_49) in (pr0 t TMP_50))))) in (let TMP_52 \def
-(Bind Abst) in (let TMP_53 \def (Flat Appl) in (let TMP_54 \def (s TMP_53 d)
-in (let TMP_55 \def (lift h TMP_54 u) in (let TMP_56 \def (Bind Abst) in (let
-TMP_57 \def (Flat Appl) in (let TMP_58 \def (s TMP_57 d) in (let TMP_59 \def
-(s TMP_56 TMP_58) in (let TMP_60 \def (lift h TMP_59 t3) in (let TMP_61 \def
-(THead TMP_52 TMP_55 TMP_60) in (let TMP_68 \def (\lambda (t: T).(let TMP_62
-\def (Flat Appl) in (let TMP_63 \def (lift h d v1) in (let TMP_64 \def (THead
-TMP_62 TMP_63 t) in (let TMP_65 \def (Bind Abbr) in (let TMP_66 \def (THead
-TMP_65 v2 t4) in (let TMP_67 \def (lift h d TMP_66) in (pr0 TMP_64
-TMP_67)))))))) in (let TMP_69 \def (Bind Abbr) in (let TMP_70 \def (lift h d
-v2) in (let TMP_71 \def (Bind Abbr) in (let TMP_72 \def (s TMP_71 d) in (let
-TMP_73 \def (lift h TMP_72 t4) in (let TMP_74 \def (THead TMP_69 TMP_70
-TMP_73) in (let TMP_88 \def (\lambda (t: T).(let TMP_75 \def (Flat Appl) in
-(let TMP_76 \def (lift h d v1) in (let TMP_77 \def (Bind Abst) in (let TMP_78
-\def (Flat Appl) in (let TMP_79 \def (s TMP_78 d) in (let TMP_80 \def (lift h
-TMP_79 u) in (let TMP_81 \def (Bind Abst) in (let TMP_82 \def (Flat Appl) in
-(let TMP_83 \def (s TMP_82 d) in (let TMP_84 \def (s TMP_81 TMP_83) in (let
-TMP_85 \def (lift h TMP_84 t3) in (let TMP_86 \def (THead TMP_77 TMP_80
-TMP_85) in (let TMP_87 \def (THead TMP_75 TMP_76 TMP_86) in (pr0 TMP_87
-t))))))))))))))) in (let TMP_89 \def (Flat Appl) in (let TMP_90 \def (s
-TMP_89 d) in (let TMP_91 \def (lift h TMP_90 u) in (let TMP_92 \def (lift h d
-v1) in (let TMP_93 \def (lift h d v2) in (let TMP_94 \def (H1 h d) in (let
-TMP_95 \def (Bind Abst) in (let TMP_96 \def (Flat Appl) in (let TMP_97 \def
-(s TMP_96 d) in (let TMP_98 \def (s TMP_95 TMP_97) in (let TMP_99 \def (lift
-h TMP_98 t3) in (let TMP_100 \def (Bind Abbr) in (let TMP_101 \def (s TMP_100
-d) in (let TMP_102 \def (lift h TMP_101 t4) in (let TMP_103 \def (Bind Abbr)
-in (let TMP_104 \def (s TMP_103 d) in (let TMP_105 \def (H3 h TMP_104) in
-(let TMP_106 \def (pr0_beta TMP_91 TMP_92 TMP_93 TMP_94 TMP_99 TMP_102
-TMP_105) in (let TMP_107 \def (Bind Abbr) in (let TMP_108 \def (THead TMP_107
-v2 t4) in (let TMP_109 \def (lift h d TMP_108) in (let TMP_110 \def (Bind
-Abbr) in (let TMP_111 \def (lift_head TMP_110 v2 t4 h d) in (let TMP_112 \def
-(eq_ind_r T TMP_74 TMP_88 TMP_106 TMP_109 TMP_111) in (let TMP_113 \def (Flat
-Appl) in (let TMP_114 \def (s TMP_113 d) in (let TMP_115 \def (Bind Abst) in
-(let TMP_116 \def (THead TMP_115 u t3) in (let TMP_117 \def (lift h TMP_114
-TMP_116) in (let TMP_118 \def (Bind Abst) in (let TMP_119 \def (Flat Appl) in
-(let TMP_120 \def (s TMP_119 d) in (let TMP_121 \def (lift_head TMP_118 u t3
-h TMP_120) in (let TMP_122 \def (eq_ind_r T TMP_61 TMP_68 TMP_112 TMP_117
-TMP_121) in (let TMP_123 \def (Flat Appl) in (let TMP_124 \def (Bind Abst) in
-(let TMP_125 \def (THead TMP_124 u t3) in (let TMP_126 \def (THead TMP_123 v1
-TMP_125) in (let TMP_127 \def (lift h d TMP_126) in (let TMP_128 \def (Flat
-Appl) in (let TMP_129 \def (Bind Abst) in (let TMP_130 \def (THead TMP_129 u
-t3) in (let TMP_131 \def (lift_head TMP_128 v1 TMP_130 h d) in (eq_ind_r T
-TMP_47 TMP_51 TMP_122 TMP_127
-TMP_131)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))) in (let TMP_339 \def (\lambda (b: B).(\lambda (H0: (not (eq B b
-Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda
-(H2: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d v1) (lift h d
-v2)))))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1 u2)).(\lambda
-(H4: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d u1) (lift h d
-u2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3 t4)).(\lambda
-(H6: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3) (lift h d
-t4)))))).(\lambda (h: nat).(\lambda (d: nat).(let TMP_133 \def (Flat Appl) in
-(let TMP_134 \def (lift h d v1) in (let TMP_135 \def (Flat Appl) in (let
-TMP_136 \def (s TMP_135 d) in (let TMP_137 \def (Bind b) in (let TMP_138 \def
-(THead TMP_137 u1 t3) in (let TMP_139 \def (lift h TMP_136 TMP_138) in (let
-TMP_140 \def (THead TMP_133 TMP_134 TMP_139) in (let TMP_148 \def (\lambda
-(t: T).(let TMP_141 \def (Bind b) in (let TMP_142 \def (Flat Appl) in (let
-TMP_143 \def (S O) in (let TMP_144 \def (lift TMP_143 O v2) in (let TMP_145
-\def (THead TMP_142 TMP_144 t4) in (let TMP_146 \def (THead TMP_141 u2
-TMP_145) in (let TMP_147 \def (lift h d TMP_146) in (pr0 t TMP_147)))))))))
-in (let TMP_149 \def (Bind b) in (let TMP_150 \def (Flat Appl) in (let
-TMP_151 \def (s TMP_150 d) in (let TMP_152 \def (lift h TMP_151 u1) in (let
-TMP_153 \def (Bind b) in (let TMP_154 \def (Flat Appl) in (let TMP_155 \def
-(s TMP_154 d) in (let TMP_156 \def (s TMP_153 TMP_155) in (let TMP_157 \def
-(lift h TMP_156 t3) in (let TMP_158 \def (THead TMP_149 TMP_152 TMP_157) in
-(let TMP_169 \def (\lambda (t: T).(let TMP_159 \def (Flat Appl) in (let
-TMP_160 \def (lift h d v1) in (let TMP_161 \def (THead TMP_159 TMP_160 t) in
-(let TMP_162 \def (Bind b) in (let TMP_163 \def (Flat Appl) in (let TMP_164
-\def (S O) in (let TMP_165 \def (lift TMP_164 O v2) in (let TMP_166 \def
-(THead TMP_163 TMP_165 t4) in (let TMP_167 \def (THead TMP_162 u2 TMP_166) in
-(let TMP_168 \def (lift h d TMP_167) in (pr0 TMP_161 TMP_168)))))))))))) in
-(let TMP_170 \def (Bind b) in (let TMP_171 \def (lift h d u2) in (let TMP_172
-\def (Bind b) in (let TMP_173 \def (s TMP_172 d) in (let TMP_174 \def (Flat
-Appl) in (let TMP_175 \def (S O) in (let TMP_176 \def (lift TMP_175 O v2) in
-(let TMP_177 \def (THead TMP_174 TMP_176 t4) in (let TMP_178 \def (lift h
-TMP_173 TMP_177) in (let TMP_179 \def (THead TMP_170 TMP_171 TMP_178) in (let
-TMP_193 \def (\lambda (t: T).(let TMP_180 \def (Flat Appl) in (let TMP_181
-\def (lift h d v1) in (let TMP_182 \def (Bind b) in (let TMP_183 \def (Flat
-Appl) in (let TMP_184 \def (s TMP_183 d) in (let TMP_185 \def (lift h TMP_184
-u1) in (let TMP_186 \def (Bind b) in (let TMP_187 \def (Flat Appl) in (let
-TMP_188 \def (s TMP_187 d) in (let TMP_189 \def (s TMP_186 TMP_188) in (let
-TMP_190 \def (lift h TMP_189 t3) in (let TMP_191 \def (THead TMP_182 TMP_185
-TMP_190) in (let TMP_192 \def (THead TMP_180 TMP_181 TMP_191) in (pr0 TMP_192
-t))))))))))))))) in (let TMP_194 \def (Flat Appl) in (let TMP_195 \def (Bind
-b) in (let TMP_196 \def (s TMP_195 d) in (let TMP_197 \def (S O) in (let
-TMP_198 \def (lift TMP_197 O v2) in (let TMP_199 \def (lift h TMP_196
-TMP_198) in (let TMP_200 \def (Flat Appl) in (let TMP_201 \def (Bind b) in
-(let TMP_202 \def (s TMP_201 d) in (let TMP_203 \def (s TMP_200 TMP_202) in
-(let TMP_204 \def (lift h TMP_203 t4) in (let TMP_205 \def (THead TMP_194
-TMP_199 TMP_204) in (let TMP_222 \def (\lambda (t: T).(let TMP_206 \def (Flat
-Appl) in (let TMP_207 \def (lift h d v1) in (let TMP_208 \def (Bind b) in
-(let TMP_209 \def (Flat Appl) in (let TMP_210 \def (s TMP_209 d) in (let
-TMP_211 \def (lift h TMP_210 u1) in (let TMP_212 \def (Bind b) in (let
-TMP_213 \def (Flat Appl) in (let TMP_214 \def (s TMP_213 d) in (let TMP_215
-\def (s TMP_212 TMP_214) in (let TMP_216 \def (lift h TMP_215 t3) in (let
-TMP_217 \def (THead TMP_208 TMP_211 TMP_216) in (let TMP_218 \def (THead
-TMP_206 TMP_207 TMP_217) in (let TMP_219 \def (Bind b) in (let TMP_220 \def
-(lift h d u2) in (let TMP_221 \def (THead TMP_219 TMP_220 t) in (pr0 TMP_218
-TMP_221)))))))))))))))))) in (let TMP_223 \def (S O) in (let TMP_224 \def
-(plus TMP_223 d) in (let TMP_241 \def (\lambda (n: nat).(let TMP_225 \def
-(Flat Appl) in (let TMP_226 \def (lift h d v1) in (let TMP_227 \def (Bind b)
-in (let TMP_228 \def (lift h d u1) in (let TMP_229 \def (lift h n t3) in (let
-TMP_230 \def (THead TMP_227 TMP_228 TMP_229) in (let TMP_231 \def (THead
-TMP_225 TMP_226 TMP_230) in (let TMP_232 \def (Bind b) in (let TMP_233 \def
-(lift h d u2) in (let TMP_234 \def (Flat Appl) in (let TMP_235 \def (S O) in
-(let TMP_236 \def (lift TMP_235 O v2) in (let TMP_237 \def (lift h n TMP_236)
-in (let TMP_238 \def (lift h n t4) in (let TMP_239 \def (THead TMP_234
-TMP_237 TMP_238) in (let TMP_240 \def (THead TMP_232 TMP_233 TMP_239) in (pr0
-TMP_231 TMP_240)))))))))))))))))) in (let TMP_242 \def (S O) in (let TMP_243
-\def (lift h d v2) in (let TMP_244 \def (lift TMP_242 O TMP_243) in (let
-TMP_262 \def (\lambda (t: T).(let TMP_245 \def (Flat Appl) in (let TMP_246
-\def (lift h d v1) in (let TMP_247 \def (Bind b) in (let TMP_248 \def (lift h
-d u1) in (let TMP_249 \def (S O) in (let TMP_250 \def (plus TMP_249 d) in
-(let TMP_251 \def (lift h TMP_250 t3) in (let TMP_252 \def (THead TMP_247
-TMP_248 TMP_251) in (let TMP_253 \def (THead TMP_245 TMP_246 TMP_252) in (let
-TMP_254 \def (Bind b) in (let TMP_255 \def (lift h d u2) in (let TMP_256 \def
-(Flat Appl) in (let TMP_257 \def (S O) in (let TMP_258 \def (plus TMP_257 d)
-in (let TMP_259 \def (lift h TMP_258 t4) in (let TMP_260 \def (THead TMP_256
-t TMP_259) in (let TMP_261 \def (THead TMP_254 TMP_255 TMP_260) in (pr0
-TMP_253 TMP_261))))))))))))))))))) in (let TMP_263 \def (lift h d v1) in (let
-TMP_264 \def (lift h d v2) in (let TMP_265 \def (H2 h d) in (let TMP_266 \def
-(lift h d u1) in (let TMP_267 \def (lift h d u2) in (let TMP_268 \def (H4 h
-d) in (let TMP_269 \def (S O) in (let TMP_270 \def (plus TMP_269 d) in (let
-TMP_271 \def (lift h TMP_270 t3) in (let TMP_272 \def (S O) in (let TMP_273
-\def (plus TMP_272 d) in (let TMP_274 \def (lift h TMP_273 t4) in (let
-TMP_275 \def (S O) in (let TMP_276 \def (plus TMP_275 d) in (let TMP_277 \def
-(H6 h TMP_276) in (let TMP_278 \def (pr0_upsilon b H0 TMP_263 TMP_264 TMP_265
-TMP_266 TMP_267 TMP_268 TMP_271 TMP_274 TMP_277) in (let TMP_279 \def (S O)
-in (let TMP_280 \def (plus TMP_279 d) in (let TMP_281 \def (S O) in (let
-TMP_282 \def (lift TMP_281 O v2) in (let TMP_283 \def (lift h TMP_280
-TMP_282) in (let TMP_284 \def (S O) in (let TMP_285 \def (le_O_n d) in (let
-TMP_286 \def (lift_d v2 h TMP_284 d O TMP_285) in (let TMP_287 \def (eq_ind_r
-T TMP_244 TMP_262 TMP_278 TMP_283 TMP_286) in (let TMP_288 \def (S d) in (let
-TMP_289 \def (S d) in (let TMP_290 \def (refl_equal nat TMP_289) in (let
-TMP_291 \def (eq_ind nat TMP_224 TMP_241 TMP_287 TMP_288 TMP_290) in (let
-TMP_292 \def (Bind b) in (let TMP_293 \def (s TMP_292 d) in (let TMP_294 \def
-(Flat Appl) in (let TMP_295 \def (S O) in (let TMP_296 \def (lift TMP_295 O
-v2) in (let TMP_297 \def (THead TMP_294 TMP_296 t4) in (let TMP_298 \def
-(lift h TMP_293 TMP_297) in (let TMP_299 \def (Flat Appl) in (let TMP_300
-\def (S O) in (let TMP_301 \def (lift TMP_300 O v2) in (let TMP_302 \def
-(Bind b) in (let TMP_303 \def (s TMP_302 d) in (let TMP_304 \def (lift_head
-TMP_299 TMP_301 t4 h TMP_303) in (let TMP_305 \def (eq_ind_r T TMP_205
-TMP_222 TMP_291 TMP_298 TMP_304) in (let TMP_306 \def (Bind b) in (let
-TMP_307 \def (Flat Appl) in (let TMP_308 \def (S O) in (let TMP_309 \def
-(lift TMP_308 O v2) in (let TMP_310 \def (THead TMP_307 TMP_309 t4) in (let
-TMP_311 \def (THead TMP_306 u2 TMP_310) in (let TMP_312 \def (lift h d
-TMP_311) in (let TMP_313 \def (Bind b) in (let TMP_314 \def (Flat Appl) in
-(let TMP_315 \def (S O) in (let TMP_316 \def (lift TMP_315 O v2) in (let
-TMP_317 \def (THead TMP_314 TMP_316 t4) in (let TMP_318 \def (lift_head
-TMP_313 u2 TMP_317 h d) in (let TMP_319 \def (eq_ind_r T TMP_179 TMP_193
-TMP_305 TMP_312 TMP_318) in (let TMP_320 \def (Flat Appl) in (let TMP_321
-\def (s TMP_320 d) in (let TMP_322 \def (Bind b) in (let TMP_323 \def (THead
-TMP_322 u1 t3) in (let TMP_324 \def (lift h TMP_321 TMP_323) in (let TMP_325
-\def (Bind b) in (let TMP_326 \def (Flat Appl) in (let TMP_327 \def (s
-TMP_326 d) in (let TMP_328 \def (lift_head TMP_325 u1 t3 h TMP_327) in (let
-TMP_329 \def (eq_ind_r T TMP_158 TMP_169 TMP_319 TMP_324 TMP_328) in (let
-TMP_330 \def (Flat Appl) in (let TMP_331 \def (Bind b) in (let TMP_332 \def
-(THead TMP_331 u1 t3) in (let TMP_333 \def (THead TMP_330 v1 TMP_332) in (let
-TMP_334 \def (lift h d TMP_333) in (let TMP_335 \def (Flat Appl) in (let
-TMP_336 \def (Bind b) in (let TMP_337 \def (THead TMP_336 u1 t3) in (let
-TMP_338 \def (lift_head TMP_335 v1 TMP_337 h d) in (eq_ind_r T TMP_140
-TMP_148 TMP_329 TMP_334
-TMP_338)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
-(let TMP_405 \def (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
+(lift h d t4)))))).(\lambda (h: nat).(\lambda (d: nat).(eq_ind_r T (THead
+(Flat Appl) (lift h d v1) (lift h (s (Flat Appl) d) (THead (Bind Abst) u
+t3))) (\lambda (t: T).(pr0 t (lift h d (THead (Bind Abbr) v2 t4)))) (eq_ind_r
+T (THead (Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s
+(Flat Appl) d)) t3)) (\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) t)
+(lift h d (THead (Bind Abbr) v2 t4)))) (eq_ind_r T (THead (Bind Abbr) (lift h
+d v2) (lift h (s (Bind Abbr) d) t4)) (\lambda (t: T).(pr0 (THead (Flat Appl)
+(lift h d v1) (THead (Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s
+(Bind Abst) (s (Flat Appl) d)) t3))) t)) (pr0_beta (lift h (s (Flat Appl) d)
+u) (lift h d v1) (lift h d v2) (H1 h d) (lift h (s (Bind Abst) (s (Flat Appl)
+d)) t3) (lift h (s (Bind Abbr) d) t4) (H3 h (s (Bind Abbr) d))) (lift h d
+(THead (Bind Abbr) v2 t4)) (lift_head (Bind Abbr) v2 t4 h d)) (lift h (s
+(Flat Appl) d) (THead (Bind Abst) u t3)) (lift_head (Bind Abst) u t3 h (s
+(Flat Appl) d))) (lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t3)))
+(lift_head (Flat Appl) v1 (THead (Bind Abst) u t3) h d))))))))))))) (\lambda
+(b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
+T).(\lambda (_: (pr0 v1 v2)).(\lambda (H2: ((\forall (h: nat).(\forall (d:
+nat).(pr0 (lift h d v1) (lift h d v2)))))).(\lambda (u1: T).(\lambda (u2:
+T).(\lambda (_: (pr0 u1 u2)).(\lambda (H4: ((\forall (h: nat).(\forall (d:
+nat).(pr0 (lift h d u1) (lift h d u2)))))).(\lambda (t3: T).(\lambda (t4:
+T).(\lambda (_: (pr0 t3 t4)).(\lambda (H6: ((\forall (h: nat).(\forall (d:
+nat).(pr0 (lift h d t3) (lift h d t4)))))).(\lambda (h: nat).(\lambda (d:
+nat).(eq_ind_r T (THead (Flat Appl) (lift h d v1) (lift h (s (Flat Appl) d)
+(THead (Bind b) u1 t3))) (\lambda (t: T).(pr0 t (lift h d (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t4))))) (eq_ind_r T (THead (Bind b)
+(lift h (s (Flat Appl) d) u1) (lift h (s (Bind b) (s (Flat Appl) d)) t3))
+(\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) t) (lift h d (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))))) (eq_ind_r T (THead
+(Bind b) (lift h d u2) (lift h (s (Bind b) d) (THead (Flat Appl) (lift (S O)
+O v2) t4))) (\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) (THead
+(Bind b) (lift h (s (Flat Appl) d) u1) (lift h (s (Bind b) (s (Flat Appl) d))
+t3))) t)) (eq_ind_r T (THead (Flat Appl) (lift h (s (Bind b) d) (lift (S O) O
+v2)) (lift h (s (Flat Appl) (s (Bind b) d)) t4)) (\lambda (t: T).(pr0 (THead
+(Flat Appl) (lift h d v1) (THead (Bind b) (lift h (s (Flat Appl) d) u1) (lift
+h (s (Bind b) (s (Flat Appl) d)) t3))) (THead (Bind b) (lift h d u2) t)))
+(eq_ind nat (plus (S O) d) (\lambda (n: nat).(pr0 (THead (Flat Appl) (lift h
+d v1) (THead (Bind b) (lift h d u1) (lift h n t3))) (THead (Bind b) (lift h d
+u2) (THead (Flat Appl) (lift h n (lift (S O) O v2)) (lift h n t4)))))
+(eq_ind_r T (lift (S O) O (lift h d v2)) (\lambda (t: T).(pr0 (THead (Flat
+Appl) (lift h d v1) (THead (Bind b) (lift h d u1) (lift h (plus (S O) d)
+t3))) (THead (Bind b) (lift h d u2) (THead (Flat Appl) t (lift h (plus (S O)
+d) t4))))) (pr0_upsilon b H0 (lift h d v1) (lift h d v2) (H2 h d) (lift h d
+u1) (lift h d u2) (H4 h d) (lift h (plus (S O) d) t3) (lift h (plus (S O) d)
+t4) (H6 h (plus (S O) d))) (lift h (plus (S O) d) (lift (S O) O v2)) (lift_d
+v2 h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d))) (lift h (s (Bind b)
+d) (THead (Flat Appl) (lift (S O) O v2) t4)) (lift_head (Flat Appl) (lift (S
+O) O v2) t4 h (s (Bind b) d))) (lift h d (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4))) (lift_head (Bind b) u2 (THead (Flat Appl) (lift
+(S O) O v2) t4) h d)) (lift h (s (Flat Appl) d) (THead (Bind b) u1 t3))
+(lift_head (Bind b) u1 t3 h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
+v1 (THead (Bind b) u1 t3))) (lift_head (Flat Appl) v1 (THead (Bind b) u1 t3)
+h d)))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1