-(CHead e (Bind b) u2))))).(let TMP_450 \def (\lambda (e: C).(let TMP_449 \def
-(CTail k u1 e) in (eq C c2 TMP_449))) in (let TMP_453 \def (\lambda (e:
-C).(let TMP_451 \def (Bind b) in (let TMP_452 \def (CHead e TMP_451 u2) in
-(getl O c TMP_452)))) in (let TMP_455 \def (\lambda (e: C).(let TMP_454 \def
-(CTail k u1 e) in (eq C c2 TMP_454))) in (let TMP_460 \def (\lambda (e:
-C).(let TMP_456 \def (Flat f) in (let TMP_457 \def (CHead c TMP_456 t) in
-(let TMP_458 \def (Bind b) in (let TMP_459 \def (CHead e TMP_458 u2) in (getl
-O TMP_457 TMP_459)))))) in (let TMP_461 \def (ex2 C TMP_455 TMP_460) in (let
-TMP_465 \def (\lambda (_: nat).(let TMP_462 \def (Flat f) in (let TMP_463
-\def (clen c) in (let TMP_464 \def (s TMP_462 TMP_463) in (eq nat O
-TMP_464))))) in (let TMP_467 \def (\lambda (_: nat).(let TMP_466 \def (Bind
-b) in (eq K k TMP_466))) in (let TMP_468 \def (\lambda (_: nat).(eq T u1 u2))
-in (let TMP_470 \def (\lambda (n: nat).(let TMP_469 \def (CSort n) in (eq C
-c2 TMP_469))) in (let TMP_471 \def (ex4 nat TMP_465 TMP_467 TMP_468 TMP_470)
-in (let TMP_472 \def (or TMP_461 TMP_471) in (let TMP_528 \def (\lambda (x:
-C).(\lambda (H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl O c (CHead x
-(Bind b) u2))).(let TMP_473 \def (CTail k u1 x) in (let TMP_492 \def (\lambda
-(c0: C).(let TMP_475 \def (\lambda (e: C).(let TMP_474 \def (CTail k u1 e) in
-(eq C c0 TMP_474))) in (let TMP_480 \def (\lambda (e: C).(let TMP_476 \def
-(Flat f) in (let TMP_477 \def (CHead c TMP_476 t) in (let TMP_478 \def (Bind
-b) in (let TMP_479 \def (CHead e TMP_478 u2) in (getl O TMP_477 TMP_479))))))
-in (let TMP_481 \def (ex2 C TMP_475 TMP_480) in (let TMP_485 \def (\lambda
-(_: nat).(let TMP_482 \def (Flat f) in (let TMP_483 \def (clen c) in (let
-TMP_484 \def (s TMP_482 TMP_483) in (eq nat O TMP_484))))) in (let TMP_487
-\def (\lambda (_: nat).(let TMP_486 \def (Bind b) in (eq K k TMP_486))) in
-(let TMP_488 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_490 \def
-(\lambda (n: nat).(let TMP_489 \def (CSort n) in (eq C c0 TMP_489))) in (let
-TMP_491 \def (ex4 nat TMP_485 TMP_487 TMP_488 TMP_490) in (or TMP_481
-TMP_491)))))))))) in (let TMP_495 \def (\lambda (e: C).(let TMP_493 \def
-(CTail k u1 x) in (let TMP_494 \def (CTail k u1 e) in (eq C TMP_493
-TMP_494)))) in (let TMP_500 \def (\lambda (e: C).(let TMP_496 \def (Flat f)
-in (let TMP_497 \def (CHead c TMP_496 t) in (let TMP_498 \def (Bind b) in
-(let TMP_499 \def (CHead e TMP_498 u2) in (getl O TMP_497 TMP_499)))))) in
-(let TMP_501 \def (ex2 C TMP_495 TMP_500) in (let TMP_505 \def (\lambda (_:
-nat).(let TMP_502 \def (Flat f) in (let TMP_503 \def (clen c) in (let TMP_504
-\def (s TMP_502 TMP_503) in (eq nat O TMP_504))))) in (let TMP_507 \def
-(\lambda (_: nat).(let TMP_506 \def (Bind b) in (eq K k TMP_506))) in (let
-TMP_508 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_511 \def (\lambda
-(n: nat).(let TMP_509 \def (CTail k u1 x) in (let TMP_510 \def (CSort n) in
-(eq C TMP_509 TMP_510)))) in (let TMP_512 \def (ex4 nat TMP_505 TMP_507
-TMP_508 TMP_511) in (let TMP_515 \def (\lambda (e: C).(let TMP_513 \def
-(CTail k u1 x) in (let TMP_514 \def (CTail k u1 e) in (eq C TMP_513
-TMP_514)))) in (let TMP_520 \def (\lambda (e: C).(let TMP_516 \def (Flat f)
-in (let TMP_517 \def (CHead c TMP_516 t) in (let TMP_518 \def (Bind b) in
-(let TMP_519 \def (CHead e TMP_518 u2) in (getl O TMP_517 TMP_519)))))) in
-(let TMP_521 \def (CTail k u1 x) in (let TMP_522 \def (refl_equal C TMP_521)
-in (let TMP_523 \def (Bind b) in (let TMP_524 \def (CHead x TMP_523 u2) in
-(let TMP_525 \def (getl_flat c TMP_524 O H5 f t) in (let TMP_526 \def
-(ex_intro2 C TMP_515 TMP_520 x TMP_522 TMP_525) in (let TMP_527 \def
-(or_introl TMP_501 TMP_512 TMP_526) in (eq_ind_r C TMP_473 TMP_492 TMP_527 c2
-H4))))))))))))))))))))))) in (ex2_ind C TMP_450 TMP_453 TMP_472 TMP_528
-H3)))))))))))))) in (let TMP_662 \def (\lambda (H3: (ex4 nat (\lambda (_:
-nat).(eq nat O (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
-nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c2 (CSort n))))).(let TMP_531 \def
-(\lambda (_: nat).(let TMP_530 \def (clen c) in (eq nat O TMP_530))) in (let
-TMP_533 \def (\lambda (_: nat).(let TMP_532 \def (Bind b) in (eq K k
-TMP_532))) in (let TMP_534 \def (\lambda (_: nat).(eq T u1 u2)) in (let
-TMP_536 \def (\lambda (n: nat).(let TMP_535 \def (CSort n) in (eq C c2
-TMP_535))) in (let TMP_538 \def (\lambda (e: C).(let TMP_537 \def (CTail k u1
-e) in (eq C c2 TMP_537))) in (let TMP_543 \def (\lambda (e: C).(let TMP_539
-\def (Flat f) in (let TMP_540 \def (CHead c TMP_539 t) in (let TMP_541 \def
-(Bind b) in (let TMP_542 \def (CHead e TMP_541 u2) in (getl O TMP_540
-TMP_542)))))) in (let TMP_544 \def (ex2 C TMP_538 TMP_543) in (let TMP_548
-\def (\lambda (_: nat).(let TMP_545 \def (Flat f) in (let TMP_546 \def (clen
-c) in (let TMP_547 \def (s TMP_545 TMP_546) in (eq nat O TMP_547))))) in (let
-TMP_550 \def (\lambda (_: nat).(let TMP_549 \def (Bind b) in (eq K k
-TMP_549))) in (let TMP_551 \def (\lambda (_: nat).(eq T u1 u2)) in (let
-TMP_553 \def (\lambda (n: nat).(let TMP_552 \def (CSort n) in (eq C c2
-TMP_552))) in (let TMP_554 \def (ex4 nat TMP_548 TMP_550 TMP_551 TMP_553) in
-(let TMP_555 \def (or TMP_544 TMP_554) in (let TMP_661 \def (\lambda (x0:
-nat).(\lambda (H4: (eq nat O (clen c))).(\lambda (H5: (eq K k (Bind
-b))).(\lambda (H6: (eq T u1 u2)).(\lambda (H7: (eq C c2 (CSort x0))).(let
-TMP_556 \def (CSort x0) in (let TMP_575 \def (\lambda (c0: C).(let TMP_558
-\def (\lambda (e: C).(let TMP_557 \def (CTail k u1 e) in (eq C c0 TMP_557)))
-in (let TMP_563 \def (\lambda (e: C).(let TMP_559 \def (Flat f) in (let
-TMP_560 \def (CHead c TMP_559 t) in (let TMP_561 \def (Bind b) in (let
-TMP_562 \def (CHead e TMP_561 u2) in (getl O TMP_560 TMP_562)))))) in (let
-TMP_564 \def (ex2 C TMP_558 TMP_563) in (let TMP_568 \def (\lambda (_:
-nat).(let TMP_565 \def (Flat f) in (let TMP_566 \def (clen c) in (let TMP_567
-\def (s TMP_565 TMP_566) in (eq nat O TMP_567))))) in (let TMP_570 \def
-(\lambda (_: nat).(let TMP_569 \def (Bind b) in (eq K k TMP_569))) in (let
-TMP_571 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_573 \def (\lambda
-(n: nat).(let TMP_572 \def (CSort n) in (eq C c0 TMP_572))) in (let TMP_574
-\def (ex4 nat TMP_568 TMP_570 TMP_571 TMP_573) in (or TMP_564
-TMP_574)))))))))) in (let TMP_596 \def (\lambda (t0: T).(let TMP_578 \def
-(\lambda (e: C).(let TMP_576 \def (CSort x0) in (let TMP_577 \def (CTail k u1
-e) in (eq C TMP_576 TMP_577)))) in (let TMP_583 \def (\lambda (e: C).(let
-TMP_579 \def (Flat f) in (let TMP_580 \def (CHead c TMP_579 t) in (let
-TMP_581 \def (Bind b) in (let TMP_582 \def (CHead e TMP_581 t0) in (getl O
-TMP_580 TMP_582)))))) in (let TMP_584 \def (ex2 C TMP_578 TMP_583) in (let
-TMP_588 \def (\lambda (_: nat).(let TMP_585 \def (Flat f) in (let TMP_586
-\def (clen c) in (let TMP_587 \def (s TMP_585 TMP_586) in (eq nat O
-TMP_587))))) in (let TMP_590 \def (\lambda (_: nat).(let TMP_589 \def (Bind
-b) in (eq K k TMP_589))) in (let TMP_591 \def (\lambda (_: nat).(eq T u1 t0))
-in (let TMP_594 \def (\lambda (n: nat).(let TMP_592 \def (CSort x0) in (let
-TMP_593 \def (CSort n) in (eq C TMP_592 TMP_593)))) in (let TMP_595 \def (ex4
-nat TMP_588 TMP_590 TMP_591 TMP_594) in (or TMP_584 TMP_595)))))))))) in (let
-TMP_597 \def (Bind b) in (let TMP_618 \def (\lambda (k1: K).(let TMP_600 \def
-(\lambda (e: C).(let TMP_598 \def (CSort x0) in (let TMP_599 \def (CTail k1
-u1 e) in (eq C TMP_598 TMP_599)))) in (let TMP_605 \def (\lambda (e: C).(let
-TMP_601 \def (Flat f) in (let TMP_602 \def (CHead c TMP_601 t) in (let
-TMP_603 \def (Bind b) in (let TMP_604 \def (CHead e TMP_603 u1) in (getl O
-TMP_602 TMP_604)))))) in (let TMP_606 \def (ex2 C TMP_600 TMP_605) in (let
-TMP_610 \def (\lambda (_: nat).(let TMP_607 \def (Flat f) in (let TMP_608
-\def (clen c) in (let TMP_609 \def (s TMP_607 TMP_608) in (eq nat O
-TMP_609))))) in (let TMP_612 \def (\lambda (_: nat).(let TMP_611 \def (Bind
-b) in (eq K k1 TMP_611))) in (let TMP_613 \def (\lambda (_: nat).(eq T u1
-u1)) in (let TMP_616 \def (\lambda (n: nat).(let TMP_614 \def (CSort x0) in
-(let TMP_615 \def (CSort n) in (eq C TMP_614 TMP_615)))) in (let TMP_617 \def
-(ex4 nat TMP_610 TMP_612 TMP_613 TMP_616) in (or TMP_606 TMP_617)))))))))) in
-(let TMP_622 \def (\lambda (e: C).(let TMP_619 \def (CSort x0) in (let
-TMP_620 \def (Bind b) in (let TMP_621 \def (CTail TMP_620 u1 e) in (eq C
-TMP_619 TMP_621))))) in (let TMP_627 \def (\lambda (e: C).(let TMP_623 \def
-(Flat f) in (let TMP_624 \def (CHead c TMP_623 t) in (let TMP_625 \def (Bind
-b) in (let TMP_626 \def (CHead e TMP_625 u1) in (getl O TMP_624 TMP_626))))))
-in (let TMP_628 \def (ex2 C TMP_622 TMP_627) in (let TMP_632 \def (\lambda
-(_: nat).(let TMP_629 \def (Flat f) in (let TMP_630 \def (clen c) in (let
-TMP_631 \def (s TMP_629 TMP_630) in (eq nat O TMP_631))))) in (let TMP_635
-\def (\lambda (_: nat).(let TMP_633 \def (Bind b) in (let TMP_634 \def (Bind
-b) in (eq K TMP_633 TMP_634)))) in (let TMP_636 \def (\lambda (_: nat).(eq T
-u1 u1)) in (let TMP_639 \def (\lambda (n: nat).(let TMP_637 \def (CSort x0)
-in (let TMP_638 \def (CSort n) in (eq C TMP_637 TMP_638)))) in (let TMP_640
-\def (ex4 nat TMP_632 TMP_635 TMP_636 TMP_639) in (let TMP_644 \def (\lambda
-(_: nat).(let TMP_641 \def (Flat f) in (let TMP_642 \def (clen c) in (let
-TMP_643 \def (s TMP_641 TMP_642) in (eq nat O TMP_643))))) in (let TMP_647
-\def (\lambda (_: nat).(let TMP_645 \def (Bind b) in (let TMP_646 \def (Bind
-b) in (eq K TMP_645 TMP_646)))) in (let TMP_648 \def (\lambda (_: nat).(eq T
-u1 u1)) in (let TMP_651 \def (\lambda (n: nat).(let TMP_649 \def (CSort x0)
-in (let TMP_650 \def (CSort n) in (eq C TMP_649 TMP_650)))) in (let TMP_652
-\def (Bind b) in (let TMP_653 \def (refl_equal K TMP_652) in (let TMP_654
-\def (refl_equal T u1) in (let TMP_655 \def (CSort x0) in (let TMP_656 \def
-(refl_equal C TMP_655) in (let TMP_657 \def (ex4_intro nat TMP_644 TMP_647
-TMP_648 TMP_651 x0 H4 TMP_653 TMP_654 TMP_656) in (let TMP_658 \def
-(or_intror TMP_628 TMP_640 TMP_657) in (let TMP_659 \def (eq_ind_r K TMP_597
-TMP_618 TMP_658 k H5) in (let TMP_660 \def (eq_ind T u1 TMP_596 TMP_659 u2
-H6) in (eq_ind_r C TMP_556 TMP_575 TMP_660 c2
-H7)))))))))))))))))))))))))))))))) in (ex4_ind nat TMP_531 TMP_533 TMP_534
-TMP_536 TMP_555 TMP_661 H3)))))))))))))))) in (or_ind TMP_421 TMP_429 TMP_448
-TMP_529 TMP_662 H2)))))))))))))))))))))))))))))))))) in (let TMP_664 \def
-(CTail k u1 c) in (let TMP_665 \def (CHead TMP_664 k0 t) in (let TMP_666 \def
-(Bind b) in (let TMP_667 \def (CHead c2 TMP_666 u2) in (let TMP_668 \def
-(getl_gen_O TMP_665 TMP_667 H0) in (K_ind TMP_262 TMP_404 TMP_663 k0
-TMP_668)))))))))) in (let TMP_1085 \def (\lambda (n: nat).(\lambda (H0:
-(((getl n (CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)) \to (or (ex2 C
-(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0
-t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen
-c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2))
-(\lambda (n0: nat).(eq C c2 (CSort n0)))))))).(\lambda (H1: (getl (S n)
-(CHead (CTail k u1 c) k0 t) (CHead c2 (Bind b) u2))).(let TMP_670 \def (r k0
-n) in (let TMP_671 \def (CTail k u1 c) in (let TMP_672 \def (Bind b) in (let
-TMP_673 \def (CHead c2 TMP_672 u2) in (let TMP_674 \def (getl_gen_S k0
-TMP_671 TMP_673 t n H1) in (let H_x \def (H TMP_670 TMP_674) in (let H2 \def
-H_x in (let TMP_676 \def (\lambda (e: C).(let TMP_675 \def (CTail k u1 e) in
-(eq C c2 TMP_675))) in (let TMP_680 \def (\lambda (e: C).(let TMP_677 \def (r
-k0 n) in (let TMP_678 \def (Bind b) in (let TMP_679 \def (CHead e TMP_678 u2)
-in (getl TMP_677 c TMP_679))))) in (let TMP_681 \def (ex2 C TMP_676 TMP_680)
-in (let TMP_684 \def (\lambda (_: nat).(let TMP_682 \def (r k0 n) in (let
-TMP_683 \def (clen c) in (eq nat TMP_682 TMP_683)))) in (let TMP_686 \def
-(\lambda (_: nat).(let TMP_685 \def (Bind b) in (eq K k TMP_685))) in (let
-TMP_687 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_689 \def (\lambda
-(n0: nat).(let TMP_688 \def (CSort n0) in (eq C c2 TMP_688))) in (let TMP_690
-\def (ex4 nat TMP_684 TMP_686 TMP_687 TMP_689) in (let TMP_692 \def (\lambda
-(e: C).(let TMP_691 \def (CTail k u1 e) in (eq C c2 TMP_691))) in (let
-TMP_697 \def (\lambda (e: C).(let TMP_693 \def (S n) in (let TMP_694 \def
-(CHead c k0 t) in (let TMP_695 \def (Bind b) in (let TMP_696 \def (CHead e
-TMP_695 u2) in (getl TMP_693 TMP_694 TMP_696)))))) in (let TMP_698 \def (ex2
-C TMP_692 TMP_697) in (let TMP_702 \def (\lambda (_: nat).(let TMP_699 \def
-(S n) in (let TMP_700 \def (clen c) in (let TMP_701 \def (s k0 TMP_700) in
-(eq nat TMP_699 TMP_701))))) in (let TMP_704 \def (\lambda (_: nat).(let
-TMP_703 \def (Bind b) in (eq K k TMP_703))) in (let TMP_705 \def (\lambda (_:
-nat).(eq T u1 u2)) in (let TMP_707 \def (\lambda (n0: nat).(let TMP_706 \def
-(CSort n0) in (eq C c2 TMP_706))) in (let TMP_708 \def (ex4 nat TMP_702
-TMP_704 TMP_705 TMP_707) in (let TMP_709 \def (or TMP_698 TMP_708) in (let
-TMP_819 \def (\lambda (H3: (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
-(\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))))).(let TMP_711 \def
-(\lambda (e: C).(let TMP_710 \def (CTail k u1 e) in (eq C c2 TMP_710))) in
-(let TMP_715 \def (\lambda (e: C).(let TMP_712 \def (r k0 n) in (let TMP_713
-\def (Bind b) in (let TMP_714 \def (CHead e TMP_713 u2) in (getl TMP_712 c
-TMP_714))))) in (let TMP_717 \def (\lambda (e: C).(let TMP_716 \def (CTail k
-u1 e) in (eq C c2 TMP_716))) in (let TMP_722 \def (\lambda (e: C).(let
-TMP_718 \def (S n) in (let TMP_719 \def (CHead c k0 t) in (let TMP_720 \def
-(Bind b) in (let TMP_721 \def (CHead e TMP_720 u2) in (getl TMP_718 TMP_719
-TMP_721)))))) in (let TMP_723 \def (ex2 C TMP_717 TMP_722) in (let TMP_727
-\def (\lambda (_: nat).(let TMP_724 \def (S n) in (let TMP_725 \def (clen c)
-in (let TMP_726 \def (s k0 TMP_725) in (eq nat TMP_724 TMP_726))))) in (let
-TMP_729 \def (\lambda (_: nat).(let TMP_728 \def (Bind b) in (eq K k
-TMP_728))) in (let TMP_730 \def (\lambda (_: nat).(eq T u1 u2)) in (let
-TMP_732 \def (\lambda (n0: nat).(let TMP_731 \def (CSort n0) in (eq C c2
-TMP_731))) in (let TMP_733 \def (ex4 nat TMP_727 TMP_729 TMP_730 TMP_732) in
-(let TMP_734 \def (or TMP_723 TMP_733) in (let TMP_818 \def (\lambda (x:
-C).(\lambda (H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl (r k0 n) c
-(CHead x (Bind b) u2))).(let TMP_739 \def (\lambda (c0: C).(let TMP_735 \def
-(r k0 n) in (let TMP_736 \def (CTail k u1 c) in (let TMP_737 \def (Bind b) in
-(let TMP_738 \def (CHead c0 TMP_737 u2) in (getl TMP_735 TMP_736
-TMP_738)))))) in (let TMP_740 \def (CTail k u1 c) in (let TMP_741 \def (Bind
-b) in (let TMP_742 \def (CHead c2 TMP_741 u2) in (let TMP_743 \def
-(getl_gen_S k0 TMP_740 TMP_742 t n H1) in (let TMP_744 \def (CTail k u1 x) in
-(let H6 \def (eq_ind C c2 TMP_739 TMP_743 TMP_744 H4) in (let TMP_761 \def
+(CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k u1
+e))) (\lambda (e: C).(getl O c (CHead e (Bind b) u2))) (or (ex2 C (\lambda
+(e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t)
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f)
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
+u2)) (\lambda (n: nat).(eq C c2 (CSort n))))) (\lambda (x: C).(\lambda (H4:
+(eq C c2 (CTail k u1 x))).(\lambda (H5: (getl O c (CHead x (Bind b)
+u2))).(eq_ind_r C (CTail k u1 x) (\lambda (c0: C).(or (ex2 C (\lambda (e:
+C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c (Flat f) t)
+(CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f)
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
+u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (or_introl (ex2 C (\lambda (e:
+C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c
+(Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
+(Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C (CTail k u1 x) (CSort n))))
+(ex_intro2 C (\lambda (e: C).(eq C (CTail k u1 x) (CTail k u1 e))) (\lambda
+(e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))) x (refl_equal C
+(CTail k u1 x)) (getl_flat c (CHead x (Bind b) u2) O H5 f t))) c2 H4)))) H3))
+(\lambda (H3: (ex4 nat (\lambda (_: nat).(eq nat O (clen c))) (\lambda (_:
+nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
+C c2 (CSort n))))).(ex4_ind nat (\lambda (_: nat).(eq nat O (clen c)))
+(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
+(n: nat).(eq C c2 (CSort n))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1
+e))) (\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u2))))
+(ex4 nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_:
+nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n: nat).(eq
+C c2 (CSort n))))) (\lambda (x0: nat).(\lambda (H4: (eq nat O (clen
+c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T u1 u2)).(\lambda
+(H7: (eq C c2 (CSort x0))).(eq_ind_r C (CSort x0) (\lambda (c0: C).(or (ex2 C
+(\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl O (CHead c
+(Flat f) t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
+(Flat f) (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
+nat).(eq T u1 u2)) (\lambda (n: nat).(eq C c0 (CSort n)))))) (eq_ind T u1
+(\lambda (t0: T).(or (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail k u1 e)))
+(\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) t0)))) (ex4
+nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq
+K k (Bind b))) (\lambda (_: nat).(eq T u1 t0)) (\lambda (n: nat).(eq C (CSort
+x0) (CSort n)))))) (eq_ind_r K (Bind b) (\lambda (k1: K).(or (ex2 C (\lambda
+(e: C).(eq C (CSort x0) (CTail k1 u1 e))) (\lambda (e: C).(getl O (CHead c
+(Flat f) t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat O (s
+(Flat f) (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b))) (\lambda (_:
+nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))))))
+(or_intror (ex2 C (\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e)))
+(\lambda (e: C).(getl O (CHead c (Flat f) t) (CHead e (Bind b) u1)))) (ex4
+nat (\lambda (_: nat).(eq nat O (s (Flat f) (clen c)))) (\lambda (_: nat).(eq
+K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n: nat).(eq C
+(CSort x0) (CSort n)))) (ex4_intro nat (\lambda (_: nat).(eq nat O (s (Flat
+f) (clen c)))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_:
+nat).(eq T u1 u1)) (\lambda (n: nat).(eq C (CSort x0) (CSort n))) x0 H4
+(refl_equal K (Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) k H5)
+u2 H6) c2 H7)))))) H3)) H2)))) k0 (getl_gen_O (CHead (CTail k u1 c) k0 t)
+(CHead c2 (Bind b) u2) H0))) (\lambda (n: nat).(\lambda (H0: (((getl n (CHead
+(CTail k u1 c) k0 t) (CHead c2 (Bind b) u2)) \to (or (ex2 C (\lambda (e:
+C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e
+(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen c))))
+(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
+(n0: nat).(eq C c2 (CSort n0)))))))).(\lambda (H1: (getl (S n) (CHead (CTail
+k u1 c) k0 t) (CHead c2 (Bind b) u2))).(let H_x \def (H (r k0 n) (getl_gen_S
+k0 (CTail k u1 c) (CHead c2 (Bind b) u2) t n H1)) in (let H2 \def H_x in
+(or_ind (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e:
+C).(getl (r k0 n) c (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq
+nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
+nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0)))) (or (ex2 C
+(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead
+c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s
+k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T
+u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (H3: (ex2 C
+(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (r k0 n) c
+(CHead e (Bind b) u2))))).(ex2_ind C (\lambda (e: C).(eq C c2 (CTail k u1
+e))) (\lambda (e: C).(getl (r k0 n) c (CHead e (Bind b) u2))) (or (ex2 C
+(\lambda (e: C).(eq C c2 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead
+c k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s
+k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T
+u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort n0))))) (\lambda (x: C).(\lambda
+(H4: (eq C c2 (CTail k u1 x))).(\lambda (H5: (getl (r k0 n) c (CHead x (Bind
+b) u2))).(let H6 \def (eq_ind C c2 (\lambda (c0: C).(getl (r k0 n) (CTail k
+u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 (CTail k u1 c) (CHead c2 (Bind
+b) u2) t n H1) (CTail k u1 x) H4) in (let H7 \def (eq_ind C c2 (\lambda (c0:
+C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0 (Bind b) u2)) \to (or (ex2
+C (\lambda (e: C).(eq C c0 (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c
+k0 t) (CHead e (Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0
+(clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1
+u2)) (\lambda (n0: nat).(eq C c0 (CSort n0))))))) H0 (CTail k u1 x) H4) in
+(eq_ind_r C (CTail k u1 x) (\lambda (c0: C).(or (ex2 C (\lambda (e: C).(eq C
+c0 (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind
+b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda
+(_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0:
+nat).(eq C c0 (CSort n0)))))) (or_introl (ex2 C (\lambda (e: C).(eq C (CTail
+k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e
+(Bind b) u2)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c))))
+(\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda
+(n0: nat).(eq C (CTail k u1 x) (CSort n0)))) (ex_intro2 C (\lambda (e: C).(eq
+C (CTail k u1 x) (CTail k u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t)
+(CHead e (Bind b) u2))) x (refl_equal C (CTail k u1 x)) (getl_head k0 n c
+(CHead x (Bind b) u2) H5 t))) c2 H4)))))) H3)) (\lambda (H3: (ex4 nat
+(\lambda (_: nat).(eq nat (r k0 n) (clen c))) (\lambda (_: nat).(eq K k (Bind
+b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2 (CSort
+n0))))).(ex4_ind nat (\lambda (_: nat).(eq nat (r k0 n) (clen c))) (\lambda
+(_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0:
+nat).(eq C c2 (CSort n0))) (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1
+e))) (\lambda (e: C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u2)))) (ex4
+nat (\lambda (_: nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K
+k (Bind b))) (\lambda (_: nat).(eq T u1 u2)) (\lambda (n0: nat).(eq C c2
+(CSort n0))))) (\lambda (x0: nat).(\lambda (H4: (eq nat (r k0 n) (clen
+c))).(\lambda (H5: (eq K k (Bind b))).(\lambda (H6: (eq T u1 u2)).(\lambda
+(H7: (eq C c2 (CSort x0))).(let H8 \def (eq_ind C c2 (\lambda (c0: C).(getl
+(r k0 n) (CTail k u1 c) (CHead c0 (Bind b) u2))) (getl_gen_S k0 (CTail k u1
+c) (CHead c2 (Bind b) u2) t n H1) (CSort x0) H7) in (let H9 \def (eq_ind C c2