-(u: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda
-(u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u
-t)))))))))).(\lambda (k: K).(let TMP_252 \def (\lambda (k0: K).(\forall (u:
-T).(\forall (d1: C).(\forall (t: T).((drop (S n0) O (CHead c0 k0 u) (CHead d1
-(Bind Abst) t)) \to (let TMP_236 \def (\lambda (d2: C).(csubt g d1 d2)) in
-(let TMP_241 \def (\lambda (d2: C).(let TMP_237 \def (S n0) in (let TMP_238
-\def (CHead c3 k0 u) in (let TMP_239 \def (Bind Abst) in (let TMP_240 \def
-(CHead d2 TMP_239 t) in (drop TMP_237 O TMP_238 TMP_240)))))) in (let TMP_242
-\def (ex2 C TMP_236 TMP_241) in (let TMP_243 \def (\lambda (d2: C).(\lambda
-(_: T).(csubt g d1 d2))) in (let TMP_248 \def (\lambda (d2: C).(\lambda (u0:
-T).(let TMP_244 \def (S n0) in (let TMP_245 \def (CHead c3 k0 u) in (let
-TMP_246 \def (Bind Abbr) in (let TMP_247 \def (CHead d2 TMP_246 u0) in (drop
-TMP_244 O TMP_245 TMP_247))))))) in (let TMP_249 \def (\lambda (_:
-C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_250 \def (\lambda (d2:
-C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_251 \def (ex4_2 C T TMP_243
-TMP_248 TMP_249 TMP_250) in (or TMP_242 TMP_251)))))))))))))) in (let TMP_403
-\def (\lambda (b: B).(\lambda (u: T).(\lambda (d1: C).(\lambda (t:
-T).(\lambda (H3: (drop (S n0) O (CHead c0 (Bind b) u) (CHead d1 (Bind Abst)
-t))).(let TMP_253 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_256 \def
-(\lambda (d2: C).(let TMP_254 \def (Bind Abst) in (let TMP_255 \def (CHead d2
-TMP_254 t) in (drop n0 O c3 TMP_255)))) in (let TMP_257 \def (ex2 C TMP_253
-TMP_256) in (let TMP_258 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1
-d2))) in (let TMP_261 \def (\lambda (d2: C).(\lambda (u0: T).(let TMP_259
-\def (Bind Abbr) in (let TMP_260 \def (CHead d2 TMP_259 u0) in (drop n0 O c3
-TMP_260))))) in (let TMP_262 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g d1
-u0 t))) in (let TMP_263 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
-t))) in (let TMP_264 \def (ex4_2 C T TMP_258 TMP_261 TMP_262 TMP_263) in (let
-TMP_265 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_271 \def (\lambda
-(d2: C).(let TMP_266 \def (S n0) in (let TMP_267 \def (Bind b) in (let
-TMP_268 \def (CHead c3 TMP_267 u) in (let TMP_269 \def (Bind Abst) in (let
-TMP_270 \def (CHead d2 TMP_269 t) in (drop TMP_266 O TMP_268 TMP_270)))))))
-in (let TMP_272 \def (ex2 C TMP_265 TMP_271) in (let TMP_273 \def (\lambda
-(d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_279 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_274 \def (S n0) in (let TMP_275 \def (Bind b) in
-(let TMP_276 \def (CHead c3 TMP_275 u) in (let TMP_277 \def (Bind Abbr) in
-(let TMP_278 \def (CHead d2 TMP_277 u0) in (drop TMP_274 O TMP_276
-TMP_278)))))))) in (let TMP_280 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g
-d1 u0 t))) in (let TMP_281 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2
-u0 t))) in (let TMP_282 \def (ex4_2 C T TMP_273 TMP_279 TMP_280 TMP_281) in
-(let TMP_283 \def (or TMP_272 TMP_282) in (let TMP_338 \def (\lambda (H4:
-(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c3
-(CHead d2 (Bind Abst) t))))).(let TMP_284 \def (\lambda (d2: C).(csubt g d1
-d2)) in (let TMP_287 \def (\lambda (d2: C).(let TMP_285 \def (Bind Abst) in
-(let TMP_286 \def (CHead d2 TMP_285 t) in (drop n0 O c3 TMP_286)))) in (let
-TMP_288 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_294 \def (\lambda
-(d2: C).(let TMP_289 \def (S n0) in (let TMP_290 \def (Bind b) in (let
-TMP_291 \def (CHead c3 TMP_290 u) in (let TMP_292 \def (Bind Abst) in (let
-TMP_293 \def (CHead d2 TMP_292 t) in (drop TMP_289 O TMP_291 TMP_293)))))))
-in (let TMP_295 \def (ex2 C TMP_288 TMP_294) in (let TMP_296 \def (\lambda
-(d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_302 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_297 \def (S n0) in (let TMP_298 \def (Bind b) in
-(let TMP_299 \def (CHead c3 TMP_298 u) in (let TMP_300 \def (Bind Abbr) in
-(let TMP_301 \def (CHead d2 TMP_300 u0) in (drop TMP_297 O TMP_299
-TMP_301)))))))) in (let TMP_303 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g
-d1 u0 t))) in (let TMP_304 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2
-u0 t))) in (let TMP_305 \def (ex4_2 C T TMP_296 TMP_302 TMP_303 TMP_304) in
-(let TMP_306 \def (or TMP_295 TMP_305) in (let TMP_337 \def (\lambda (x:
-C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6: (drop n0 O c3 (CHead x (Bind
-Abst) t))).(let TMP_307 \def (\lambda (d2: C).(csubt g d1 d2)) in (let
-TMP_313 \def (\lambda (d2: C).(let TMP_308 \def (S n0) in (let TMP_309 \def
-(Bind b) in (let TMP_310 \def (CHead c3 TMP_309 u) in (let TMP_311 \def (Bind
-Abst) in (let TMP_312 \def (CHead d2 TMP_311 t) in (drop TMP_308 O TMP_310
-TMP_312))))))) in (let TMP_314 \def (ex2 C TMP_307 TMP_313) in (let TMP_315
-\def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_321 \def
-(\lambda (d2: C).(\lambda (u0: T).(let TMP_316 \def (S n0) in (let TMP_317
-\def (Bind b) in (let TMP_318 \def (CHead c3 TMP_317 u) in (let TMP_319 \def
-(Bind Abbr) in (let TMP_320 \def (CHead d2 TMP_319 u0) in (drop TMP_316 O
-TMP_318 TMP_320)))))))) in (let TMP_322 \def (\lambda (_: C).(\lambda (u0:
-T).(ty3 g d1 u0 t))) in (let TMP_323 \def (\lambda (d2: C).(\lambda (u0:
-T).(ty3 g d2 u0 t))) in (let TMP_324 \def (ex4_2 C T TMP_315 TMP_321 TMP_322
-TMP_323) in (let TMP_325 \def (\lambda (d2: C).(csubt g d1 d2)) in (let
-TMP_331 \def (\lambda (d2: C).(let TMP_326 \def (S n0) in (let TMP_327 \def
-(Bind b) in (let TMP_328 \def (CHead c3 TMP_327 u) in (let TMP_329 \def (Bind
-Abst) in (let TMP_330 \def (CHead d2 TMP_329 t) in (drop TMP_326 O TMP_328
-TMP_330))))))) in (let TMP_332 \def (Bind b) in (let TMP_333 \def (Bind Abst)
-in (let TMP_334 \def (CHead x TMP_333 t) in (let TMP_335 \def (drop_drop
-TMP_332 n0 c3 TMP_334 H6 u) in (let TMP_336 \def (ex_intro2 C TMP_325 TMP_331
-x H5 TMP_335) in (or_introl TMP_314 TMP_324 TMP_336))))))))))))))))))) in
-(ex2_ind C TMP_284 TMP_287 TMP_306 TMP_337 H4)))))))))))))) in (let TMP_397
-\def (\lambda (H4: (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
-d2))) (\lambda (d2: C).(\lambda (u0: T).(drop n0 O c3 (CHead d2 (Bind Abbr)
-u0)))) (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2:
-C).(\lambda (u0: T).(ty3 g d2 u0 t))))).(let TMP_339 \def (\lambda (d2:
-C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_342 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_340 \def (Bind Abbr) in (let TMP_341 \def (CHead
-d2 TMP_340 u0) in (drop n0 O c3 TMP_341))))) in (let TMP_343 \def (\lambda
-(_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_344 \def (\lambda (d2:
-C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_345 \def (\lambda (d2:
-C).(csubt g d1 d2)) in (let TMP_351 \def (\lambda (d2: C).(let TMP_346 \def
-(S n0) in (let TMP_347 \def (Bind b) in (let TMP_348 \def (CHead c3 TMP_347
-u) in (let TMP_349 \def (Bind Abst) in (let TMP_350 \def (CHead d2 TMP_349 t)
-in (drop TMP_346 O TMP_348 TMP_350))))))) in (let TMP_352 \def (ex2 C TMP_345
-TMP_351) in (let TMP_353 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1
-d2))) in (let TMP_359 \def (\lambda (d2: C).(\lambda (u0: T).(let TMP_354
-\def (S n0) in (let TMP_355 \def (Bind b) in (let TMP_356 \def (CHead c3
-TMP_355 u) in (let TMP_357 \def (Bind Abbr) in (let TMP_358 \def (CHead d2
-TMP_357 u0) in (drop TMP_354 O TMP_356 TMP_358)))))))) in (let TMP_360 \def
-(\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_361 \def
-(\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_362 \def
-(ex4_2 C T TMP_353 TMP_359 TMP_360 TMP_361) in (let TMP_363 \def (or TMP_352
-TMP_362) in (let TMP_396 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda (H5:
-(csubt g d1 x0)).(\lambda (H6: (drop n0 O c3 (CHead x0 (Bind Abbr)
-x1))).(\lambda (H7: (ty3 g d1 x1 t)).(\lambda (H8: (ty3 g x0 x1 t)).(let
-TMP_364 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_370 \def (\lambda
-(d2: C).(let TMP_365 \def (S n0) in (let TMP_366 \def (Bind b) in (let
-TMP_367 \def (CHead c3 TMP_366 u) in (let TMP_368 \def (Bind Abst) in (let
-TMP_369 \def (CHead d2 TMP_368 t) in (drop TMP_365 O TMP_367 TMP_369)))))))
-in (let TMP_371 \def (ex2 C TMP_364 TMP_370) in (let TMP_372 \def (\lambda
-(d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_378 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_373 \def (S n0) in (let TMP_374 \def (Bind b) in
-(let TMP_375 \def (CHead c3 TMP_374 u) in (let TMP_376 \def (Bind Abbr) in
-(let TMP_377 \def (CHead d2 TMP_376 u0) in (drop TMP_373 O TMP_375
-TMP_377)))))))) in (let TMP_379 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g
-d1 u0 t))) in (let TMP_380 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2
-u0 t))) in (let TMP_381 \def (ex4_2 C T TMP_372 TMP_378 TMP_379 TMP_380) in
-(let TMP_382 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let
-TMP_388 \def (\lambda (d2: C).(\lambda (u0: T).(let TMP_383 \def (S n0) in
-(let TMP_384 \def (Bind b) in (let TMP_385 \def (CHead c3 TMP_384 u) in (let
-TMP_386 \def (Bind Abbr) in (let TMP_387 \def (CHead d2 TMP_386 u0) in (drop
-TMP_383 O TMP_385 TMP_387)))))))) in (let TMP_389 \def (\lambda (_:
-C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_390 \def (\lambda (d2:
-C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_391 \def (Bind b) in (let
-TMP_392 \def (Bind Abbr) in (let TMP_393 \def (CHead x0 TMP_392 x1) in (let
-TMP_394 \def (drop_drop TMP_391 n0 c3 TMP_393 H6 u) in (let TMP_395 \def
-(ex4_2_intro C T TMP_382 TMP_388 TMP_389 TMP_390 x0 x1 H5 TMP_394 H7 H8) in
-(or_intror TMP_371 TMP_381 TMP_395)))))))))))))))))))))))) in (ex4_2_ind C T
-TMP_339 TMP_342 TMP_343 TMP_344 TMP_363 TMP_396 H4)))))))))))))))) in (let
-TMP_398 \def (Bind b) in (let TMP_399 \def (Bind Abst) in (let TMP_400 \def
-(CHead d1 TMP_399 t) in (let TMP_401 \def (drop_gen_drop TMP_398 c0 TMP_400 u
-n0 H3) in (let TMP_402 \def (H c0 c3 H1 d1 t TMP_401) in (or_ind TMP_257
-TMP_264 TMP_283 TMP_338 TMP_397 TMP_402)))))))))))))))))))))))))))))) in (let
-TMP_558 \def (\lambda (f: F).(\lambda (u: T).(\lambda (d1: C).(\lambda (t:
-T).(\lambda (H3: (drop (S n0) O (CHead c0 (Flat f) u) (CHead d1 (Bind Abst)
-t))).(let TMP_404 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_408 \def
-(\lambda (d2: C).(let TMP_405 \def (S n0) in (let TMP_406 \def (Bind Abst) in
-(let TMP_407 \def (CHead d2 TMP_406 t) in (drop TMP_405 O c3 TMP_407))))) in
-(let TMP_409 \def (ex2 C TMP_404 TMP_408) in (let TMP_410 \def (\lambda (d2:
-C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_414 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_411 \def (S n0) in (let TMP_412 \def (Bind Abbr)
-in (let TMP_413 \def (CHead d2 TMP_412 u0) in (drop TMP_411 O c3
-TMP_413)))))) in (let TMP_415 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g d1
-u0 t))) in (let TMP_416 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0
-t))) in (let TMP_417 \def (ex4_2 C T TMP_410 TMP_414 TMP_415 TMP_416) in (let
-TMP_418 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_424 \def (\lambda
-(d2: C).(let TMP_419 \def (S n0) in (let TMP_420 \def (Flat f) in (let
-TMP_421 \def (CHead c3 TMP_420 u) in (let TMP_422 \def (Bind Abst) in (let
-TMP_423 \def (CHead d2 TMP_422 t) in (drop TMP_419 O TMP_421 TMP_423)))))))
-in (let TMP_425 \def (ex2 C TMP_418 TMP_424) in (let TMP_426 \def (\lambda
-(d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_432 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_427 \def (S n0) in (let TMP_428 \def (Flat f) in
-(let TMP_429 \def (CHead c3 TMP_428 u) in (let TMP_430 \def (Bind Abbr) in
-(let TMP_431 \def (CHead d2 TMP_430 u0) in (drop TMP_427 O TMP_429
-TMP_431)))))))) in (let TMP_433 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g
-d1 u0 t))) in (let TMP_434 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2
-u0 t))) in (let TMP_435 \def (ex4_2 C T TMP_426 TMP_432 TMP_433 TMP_434) in
-(let TMP_436 \def (or TMP_425 TMP_435) in (let TMP_492 \def (\lambda (H4:
-(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O c3
-(CHead d2 (Bind Abst) t))))).(let TMP_437 \def (\lambda (d2: C).(csubt g d1
-d2)) in (let TMP_441 \def (\lambda (d2: C).(let TMP_438 \def (S n0) in (let
-TMP_439 \def (Bind Abst) in (let TMP_440 \def (CHead d2 TMP_439 t) in (drop
-TMP_438 O c3 TMP_440))))) in (let TMP_442 \def (\lambda (d2: C).(csubt g d1
-d2)) in (let TMP_448 \def (\lambda (d2: C).(let TMP_443 \def (S n0) in (let
-TMP_444 \def (Flat f) in (let TMP_445 \def (CHead c3 TMP_444 u) in (let
-TMP_446 \def (Bind Abst) in (let TMP_447 \def (CHead d2 TMP_446 t) in (drop
-TMP_443 O TMP_445 TMP_447))))))) in (let TMP_449 \def (ex2 C TMP_442 TMP_448)
-in (let TMP_450 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in
-(let TMP_456 \def (\lambda (d2: C).(\lambda (u0: T).(let TMP_451 \def (S n0)
-in (let TMP_452 \def (Flat f) in (let TMP_453 \def (CHead c3 TMP_452 u) in
-(let TMP_454 \def (Bind Abbr) in (let TMP_455 \def (CHead d2 TMP_454 u0) in
-(drop TMP_451 O TMP_453 TMP_455)))))))) in (let TMP_457 \def (\lambda (_:
-C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_458 \def (\lambda (d2:
-C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_459 \def (ex4_2 C T TMP_450
-TMP_456 TMP_457 TMP_458) in (let TMP_460 \def (or TMP_449 TMP_459) in (let
-TMP_491 \def (\lambda (x: C).(\lambda (H5: (csubt g d1 x)).(\lambda (H6:
-(drop (S n0) O c3 (CHead x (Bind Abst) t))).(let TMP_461 \def (\lambda (d2:
-C).(csubt g d1 d2)) in (let TMP_467 \def (\lambda (d2: C).(let TMP_462 \def
-(S n0) in (let TMP_463 \def (Flat f) in (let TMP_464 \def (CHead c3 TMP_463
-u) in (let TMP_465 \def (Bind Abst) in (let TMP_466 \def (CHead d2 TMP_465 t)
-in (drop TMP_462 O TMP_464 TMP_466))))))) in (let TMP_468 \def (ex2 C TMP_461
-TMP_467) in (let TMP_469 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1
-d2))) in (let TMP_475 \def (\lambda (d2: C).(\lambda (u0: T).(let TMP_470
-\def (S n0) in (let TMP_471 \def (Flat f) in (let TMP_472 \def (CHead c3
-TMP_471 u) in (let TMP_473 \def (Bind Abbr) in (let TMP_474 \def (CHead d2
-TMP_473 u0) in (drop TMP_470 O TMP_472 TMP_474)))))))) in (let TMP_476 \def
-(\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_477 \def
-(\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_478 \def
-(ex4_2 C T TMP_469 TMP_475 TMP_476 TMP_477) in (let TMP_479 \def (\lambda
-(d2: C).(csubt g d1 d2)) in (let TMP_485 \def (\lambda (d2: C).(let TMP_480
-\def (S n0) in (let TMP_481 \def (Flat f) in (let TMP_482 \def (CHead c3
-TMP_481 u) in (let TMP_483 \def (Bind Abst) in (let TMP_484 \def (CHead d2
-TMP_483 t) in (drop TMP_480 O TMP_482 TMP_484))))))) in (let TMP_486 \def
-(Flat f) in (let TMP_487 \def (Bind Abst) in (let TMP_488 \def (CHead x
-TMP_487 t) in (let TMP_489 \def (drop_drop TMP_486 n0 c3 TMP_488 H6 u) in
-(let TMP_490 \def (ex_intro2 C TMP_479 TMP_485 x H5 TMP_489) in (or_introl
-TMP_468 TMP_478 TMP_490))))))))))))))))))) in (ex2_ind C TMP_437 TMP_441
-TMP_460 TMP_491 H4)))))))))))))) in (let TMP_552 \def (\lambda (H4: (ex4_2 C
-T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
-C).(\lambda (u0: T).(drop (S n0) O c3 (CHead d2 (Bind Abbr) u0)))) (\lambda
-(_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) (\lambda (d2: C).(\lambda (u0:
-T).(ty3 g d2 u0 t))))).(let TMP_493 \def (\lambda (d2: C).(\lambda (_:
-T).(csubt g d1 d2))) in (let TMP_497 \def (\lambda (d2: C).(\lambda (u0:
-T).(let TMP_494 \def (S n0) in (let TMP_495 \def (Bind Abbr) in (let TMP_496
-\def (CHead d2 TMP_495 u0) in (drop TMP_494 O c3 TMP_496)))))) in (let
-TMP_498 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let
-TMP_499 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let
-TMP_500 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_506 \def (\lambda
-(d2: C).(let TMP_501 \def (S n0) in (let TMP_502 \def (Flat f) in (let
-TMP_503 \def (CHead c3 TMP_502 u) in (let TMP_504 \def (Bind Abst) in (let
-TMP_505 \def (CHead d2 TMP_504 t) in (drop TMP_501 O TMP_503 TMP_505)))))))
-in (let TMP_507 \def (ex2 C TMP_500 TMP_506) in (let TMP_508 \def (\lambda
-(d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_514 \def (\lambda (d2:
-C).(\lambda (u0: T).(let TMP_509 \def (S n0) in (let TMP_510 \def (Flat f) in
-(let TMP_511 \def (CHead c3 TMP_510 u) in (let TMP_512 \def (Bind Abbr) in
-(let TMP_513 \def (CHead d2 TMP_512 u0) in (drop TMP_509 O TMP_511
-TMP_513)))))))) in (let TMP_515 \def (\lambda (_: C).(\lambda (u0: T).(ty3 g
-d1 u0 t))) in (let TMP_516 \def (\lambda (d2: C).(\lambda (u0: T).(ty3 g d2
-u0 t))) in (let TMP_517 \def (ex4_2 C T TMP_508 TMP_514 TMP_515 TMP_516) in
-(let TMP_518 \def (or TMP_507 TMP_517) in (let TMP_551 \def (\lambda (x0:
-C).(\lambda (x1: T).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (drop (S n0)
-O c3 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g d1 x1 t)).(\lambda (H8:
-(ty3 g x0 x1 t)).(let TMP_519 \def (\lambda (d2: C).(csubt g d1 d2)) in (let
-TMP_525 \def (\lambda (d2: C).(let TMP_520 \def (S n0) in (let TMP_521 \def
-(Flat f) in (let TMP_522 \def (CHead c3 TMP_521 u) in (let TMP_523 \def (Bind
-Abst) in (let TMP_524 \def (CHead d2 TMP_523 t) in (drop TMP_520 O TMP_522
-TMP_524))))))) in (let TMP_526 \def (ex2 C TMP_519 TMP_525) in (let TMP_527
-\def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_533 \def
-(\lambda (d2: C).(\lambda (u0: T).(let TMP_528 \def (S n0) in (let TMP_529
-\def (Flat f) in (let TMP_530 \def (CHead c3 TMP_529 u) in (let TMP_531 \def
-(Bind Abbr) in (let TMP_532 \def (CHead d2 TMP_531 u0) in (drop TMP_528 O
-TMP_530 TMP_532)))))))) in (let TMP_534 \def (\lambda (_: C).(\lambda (u0:
-T).(ty3 g d1 u0 t))) in (let TMP_535 \def (\lambda (d2: C).(\lambda (u0:
-T).(ty3 g d2 u0 t))) in (let TMP_536 \def (ex4_2 C T TMP_527 TMP_533 TMP_534
-TMP_535) in (let TMP_537 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1
-d2))) in (let TMP_543 \def (\lambda (d2: C).(\lambda (u0: T).(let TMP_538
-\def (S n0) in (let TMP_539 \def (Flat f) in (let TMP_540 \def (CHead c3
-TMP_539 u) in (let TMP_541 \def (Bind Abbr) in (let TMP_542 \def (CHead d2
-TMP_541 u0) in (drop TMP_538 O TMP_540 TMP_542)))))))) in (let TMP_544 \def
-(\lambda (_: C).(\lambda (u0: T).(ty3 g d1 u0 t))) in (let TMP_545 \def
-(\lambda (d2: C).(\lambda (u0: T).(ty3 g d2 u0 t))) in (let TMP_546 \def
-(Flat f) in (let TMP_547 \def (Bind Abbr) in (let TMP_548 \def (CHead x0
-TMP_547 x1) in (let TMP_549 \def (drop_drop TMP_546 n0 c3 TMP_548 H6 u) in
-(let TMP_550 \def (ex4_2_intro C T TMP_537 TMP_543 TMP_544 TMP_545 x0 x1 H5
-TMP_549 H7 H8) in (or_intror TMP_526 TMP_536 TMP_550))))))))))))))))))))))))
-in (ex4_2_ind C T TMP_493 TMP_497 TMP_498 TMP_499 TMP_518 TMP_551
-H4)))))))))))))))) in (let TMP_553 \def (Flat f) in (let TMP_554 \def (Bind
-Abst) in (let TMP_555 \def (CHead d1 TMP_554 t) in (let TMP_556 \def
-(drop_gen_drop TMP_553 c0 TMP_555 u n0 H3) in (let TMP_557 \def (H2 d1 t
-TMP_556) in (or_ind TMP_409 TMP_417 TMP_436 TMP_492 TMP_552
-TMP_557)))))))))))))))))))))))))))))) in (K_ind TMP_252 TMP_403 TMP_558
-k))))))))) in (let TMP_710 \def (\lambda (c0: C).(\lambda (c3: C).(\lambda
-(H1: (csubt g c0 c3)).(\lambda (_: ((\forall (d1: C).(\forall (t: T).((drop
+(u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
+T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))
+(\lambda (x: C).(\lambda (H4: (eq C c2 (CHead x (Bind Abst) t))).(\lambda
+(H5: (csubt g d1 x)).(eq_ind_r C (CHead x (Bind Abst) t) (\lambda (c: C).(or
+(ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c (CHead
+d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O c (CHead d2 (Bind Abbr)
+u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
+C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_introl (ex2 C (\lambda (d2:
+C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead
+d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x (Bind Abst) t)
+(CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
+(\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))) (ex_intro2 C (\lambda (d2:
+C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x (Bind Abst) t) (CHead
+d2 (Bind Abst) t))) x H5 (drop_refl (CHead x (Bind Abst) t)))) c2 H4)))) H3))
+(\lambda (H3: (ex4_2 C T (\lambda (e2: C).(\lambda (v2: T).(eq C c2 (CHead e2
+(Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2)))
+(\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t))) (\lambda (e2: C).(\lambda
+(v2: T).(ty3 g e2 v2 t))))).(ex4_2_ind C T (\lambda (e2: C).(\lambda (v2:
+T).(eq C c2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2: C).(\lambda (_:
+T).(csubt g d1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t)))
+(\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))) (or (ex2 C (\lambda (d2:
+C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O c2 (CHead d2 (Bind Abst) t))))
+(ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
+C).(\lambda (u: T).(drop O O c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_:
+C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g
+d2 u t))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead
+x0 (Bind Abbr) x1))).(\lambda (H5: (csubt g d1 x0)).(\lambda (H6: (ty3 g d1
+x1 t)).(\lambda (H7: (ty3 g x0 x1 t)).(eq_ind_r C (CHead x0 (Bind Abbr) x1)
+(\lambda (c: C).(or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2:
+C).(drop O O c (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2:
+C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O
+O c (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
+t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))) (or_intror (ex2 C
+(\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop O O (CHead x0 (Bind
+Abbr) x1) (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
+(_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop O O (CHead x0
+(Bind Abbr) x1) (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u:
+T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))
+(ex4_2_intro C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda
+(d2: C).(\lambda (u: T).(drop O O (CHead x0 (Bind Abbr) x1) (CHead d2 (Bind
+Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
+C).(\lambda (u: T).(ty3 g d2 u t))) x0 x1 H5 (drop_refl (CHead x0 (Bind Abbr)
+x1)) H6 H7)) c2 H4))))))) H3)) H2))))))))) (\lambda (n0: nat).(\lambda (H:
+((\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (\forall (d1:
+C).(\forall (t: T).((drop n0 O c1 (CHead d1 (Bind Abst) t)) \to (or (ex2 C
+(\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop n0 O c2 (CHead d2
+(Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop n0 O c2 (CHead d2 (Bind Abbr)
+u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2:
+C).(\lambda (u: T).(ty3 g d2 u t))))))))))))).(\lambda (c1: C).(\lambda (c2:
+C).(\lambda (H0: (csubt g c1 c2)).(csubt_ind g (\lambda (c: C).(\lambda (c0:
+C).(\forall (d1: C).(\forall (t: T).((drop (S n0) O c (CHead d1 (Bind Abst)
+t)) \to (or (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop
+(S n0) O c0 (CHead d2 (Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda
+(_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O c0
+(CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t)))
+(\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))))))))) (\lambda (n1:
+nat).(\lambda (d1: C).(\lambda (t: T).(\lambda (H1: (drop (S n0) O (CSort n1)
+(CHead d1 (Bind Abst) t))).(and3_ind (eq C (CHead d1 (Bind Abst) t) (CSort
+n1)) (eq nat (S n0) O) (eq nat O O) (or (ex2 C (\lambda (d2: C).(csubt g d1
+d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abst) t))))
+(ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2:
+C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2 (Bind Abbr) u))))
+(\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda
+(u: T).(ty3 g d2 u t))))) (\lambda (_: (eq C (CHead d1 (Bind Abst) t) (CSort
+n1))).(\lambda (H3: (eq nat (S n0) O)).(\lambda (_: (eq nat O O)).(let H5
+\def (eq_ind nat (S n0) (\lambda (ee: nat).(match ee with [O \Rightarrow
+False | (S _) \Rightarrow True])) I O H3) in (False_ind (or (ex2 C (\lambda
+(d2: C).(csubt g d1 d2)) (\lambda (d2: C).(drop (S n0) O (CSort n1) (CHead d2
+(Bind Abst) t)))) (ex4_2 C T (\lambda (d2: C).(\lambda (_: T).(csubt g d1
+d2))) (\lambda (d2: C).(\lambda (u: T).(drop (S n0) O (CSort n1) (CHead d2
+(Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) (\lambda
+(d2: C).(\lambda (u: T).(ty3 g d2 u t))))) H5))))) (drop_gen_sort n1 (S n0) O
+(CHead d1 (Bind Abst) t) H1)))))) (\lambda (c0: C).(\lambda (c3: C).(\lambda
+(H1: (csubt g c0 c3)).(\lambda (H2: ((\forall (d1: C).(\forall (t: T).((drop