-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 (\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 (CSort x0) H7) in (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 (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)))))) (let H10 \def (eq_ind_r T u2 (\lambda (t0: T).((getl n (CHead (CTail
-k u1 c) k0 t) (CHead (CSort x0) (Bind b) t0)) \to (or (ex2 C (\lambda (e:
-C).(eq C (CSort x0) (CTail k u1 e))) (\lambda (e: C).(getl n (CHead c k0 t)
-(CHead e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen
-c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_: nat).(eq T u1 t0))
-(\lambda (n0: nat).(eq C (CSort x0) (CSort n0))))))) H9 u1 H6) in (let H11
-\def (eq_ind_r T u2 (\lambda (t0: T).(getl (r k0 n) (CTail k u1 c) (CHead
-(CSort x0) (Bind b) t0))) H8 u1 H6) in (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 (S
-n) (CHead c k0 t) (CHead e (Bind b) t0)))) (ex4 nat (\lambda (_: nat).(eq nat
-(S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k (Bind b))) (\lambda (_:
-nat).(eq T u1 t0)) (\lambda (n0: nat).(eq C (CSort x0) (CSort n0)))))) (let
-H12 \def (eq_ind K k (\lambda (k1: K).((getl n (CHead (CTail k1 u1 c) k0 t)
-(CHead (CSort x0) (Bind b) u1)) \to (or (ex2 C (\lambda (e: C).(eq C (CSort
-x0) (CTail k1 u1 e))) (\lambda (e: C).(getl n (CHead c k0 t) (CHead e (Bind
-b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat n (s k0 (clen c)))) (\lambda (_:
-nat).(eq K k1 (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0:
-nat).(eq C (CSort x0) (CSort n0))))))) H10 (Bind b) H5) in (let H13 \def
-(eq_ind K k (\lambda (k1: K).(getl (r k0 n) (CTail k1 u1 c) (CHead (CSort x0)
-(Bind b) u1))) H11 (Bind b) H5) in (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 (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_:
-nat).(eq nat (S n) (s k0 (clen c)))) (\lambda (_: nat).(eq K k1 (Bind b)))
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort
-n0)))))) (eq_ind nat (r k0 n) (\lambda (n0: nat).(or (ex2 C (\lambda (e:
-C).(eq C (CSort x0) (CTail (Bind b) u1 e))) (\lambda (e: C).(getl (S n)
-(CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S
-n) (s k0 n0))) (\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_:
-nat).(eq T u1 u1)) (\lambda (n1: nat).(eq C (CSort x0) (CSort n1))))))
-(eq_ind_r nat (S n) (\lambda (n0: nat).(or (ex2 C (\lambda (e: C).(eq C
-(CSort x0) (CTail (Bind b) u1 e))) (\lambda (e: C).(getl (S n) (CHead c k0 t)
-(CHead e (Bind b) u1)))) (ex4 nat (\lambda (_: nat).(eq nat (S n) n0))
-(\lambda (_: nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1))
-(\lambda (n1: nat).(eq C (CSort x0) (CSort n1)))))) (or_intror (ex2 C
-(\lambda (e: C).(eq C (CSort x0) (CTail (Bind b) u1 e))) (\lambda (e:
-C).(getl (S n) (CHead c k0 t) (CHead e (Bind b) u1)))) (ex4 nat (\lambda (_:
-nat).(eq nat (S n) (S n))) (\lambda (_: nat).(eq K (Bind b) (Bind b)))
-(\lambda (_: nat).(eq T u1 u1)) (\lambda (n0: nat).(eq C (CSort x0) (CSort
-n0)))) (ex4_intro nat (\lambda (_: nat).(eq nat (S n) (S n))) (\lambda (_:
-nat).(eq K (Bind b) (Bind b))) (\lambda (_: nat).(eq T u1 u1)) (\lambda (n0:
-nat).(eq C (CSort x0) (CSort n0))) x0 (refl_equal nat (S n)) (refl_equal K
-(Bind b)) (refl_equal T u1) (refl_equal C (CSort x0)))) (s k0 (r k0 n)) (s_r
-k0 n)) (clen c) H4) k H5))) u2 H6))) c2 H7)))))))) H3)) H2)))))) i))))))
-c1)))))).
-(* COMMENTS
-Initial nodes: 7489
-END *)
+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
+(\lambda (c0: C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0 (Bind b) u2))
+\to (let TMP_746 \def (\lambda (e: C).(let TMP_745 \def (CTail k u1 e) in (eq
+C c0 TMP_745))) in (let TMP_750 \def (\lambda (e: C).(let TMP_747 \def (CHead
+c k0 t) in (let TMP_748 \def (Bind b) in (let TMP_749 \def (CHead e TMP_748
+u2) in (getl n TMP_747 TMP_749))))) in (let TMP_751 \def (ex2 C TMP_746
+TMP_750) in (let TMP_754 \def (\lambda (_: nat).(let TMP_752 \def (clen c) in
+(let TMP_753 \def (s k0 TMP_752) in (eq nat n TMP_753)))) in (let TMP_756
+\def (\lambda (_: nat).(let TMP_755 \def (Bind b) in (eq K k TMP_755))) in
+(let TMP_757 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_759 \def
+(\lambda (n0: nat).(let TMP_758 \def (CSort n0) in (eq C c0 TMP_758))) in
+(let TMP_760 \def (ex4 nat TMP_754 TMP_756 TMP_757 TMP_759) in (or TMP_751
+TMP_760))))))))))) in (let TMP_762 \def (CTail k u1 x) in (let H7 \def
+(eq_ind C c2 TMP_761 H0 TMP_762 H4) in (let TMP_763 \def (CTail k u1 x) in
+(let TMP_782 \def (\lambda (c0: C).(let TMP_765 \def (\lambda (e: C).(let
+TMP_764 \def (CTail k u1 e) in (eq C c0 TMP_764))) in (let TMP_770 \def
+(\lambda (e: C).(let TMP_766 \def (S n) in (let TMP_767 \def (CHead c k0 t)
+in (let TMP_768 \def (Bind b) in (let TMP_769 \def (CHead e TMP_768 u2) in
+(getl TMP_766 TMP_767 TMP_769)))))) in (let TMP_771 \def (ex2 C TMP_765
+TMP_770) in (let TMP_775 \def (\lambda (_: nat).(let TMP_772 \def (S n) in
+(let TMP_773 \def (clen c) in (let TMP_774 \def (s k0 TMP_773) in (eq nat
+TMP_772 TMP_774))))) in (let TMP_777 \def (\lambda (_: nat).(let TMP_776 \def
+(Bind b) in (eq K k TMP_776))) in (let TMP_778 \def (\lambda (_: nat).(eq T
+u1 u2)) in (let TMP_780 \def (\lambda (n0: nat).(let TMP_779 \def (CSort n0)
+in (eq C c0 TMP_779))) in (let TMP_781 \def (ex4 nat TMP_775 TMP_777 TMP_778
+TMP_780) in (or TMP_771 TMP_781)))))))))) in (let TMP_785 \def (\lambda (e:
+C).(let TMP_783 \def (CTail k u1 x) in (let TMP_784 \def (CTail k u1 e) in
+(eq C TMP_783 TMP_784)))) in (let TMP_790 \def (\lambda (e: C).(let TMP_786
+\def (S n) in (let TMP_787 \def (CHead c k0 t) in (let TMP_788 \def (Bind b)
+in (let TMP_789 \def (CHead e TMP_788 u2) in (getl TMP_786 TMP_787
+TMP_789)))))) in (let TMP_791 \def (ex2 C TMP_785 TMP_790) in (let TMP_795
+\def (\lambda (_: nat).(let TMP_792 \def (S n) in (let TMP_793 \def (clen c)
+in (let TMP_794 \def (s k0 TMP_793) in (eq nat TMP_792 TMP_794))))) in (let
+TMP_797 \def (\lambda (_: nat).(let TMP_796 \def (Bind b) in (eq K k
+TMP_796))) in (let TMP_798 \def (\lambda (_: nat).(eq T u1 u2)) in (let
+TMP_801 \def (\lambda (n0: nat).(let TMP_799 \def (CTail k u1 x) in (let
+TMP_800 \def (CSort n0) in (eq C TMP_799 TMP_800)))) in (let TMP_802 \def
+(ex4 nat TMP_795 TMP_797 TMP_798 TMP_801) in (let TMP_805 \def (\lambda (e:
+C).(let TMP_803 \def (CTail k u1 x) in (let TMP_804 \def (CTail k u1 e) in
+(eq C TMP_803 TMP_804)))) in (let TMP_810 \def (\lambda (e: C).(let TMP_806
+\def (S n) in (let TMP_807 \def (CHead c k0 t) in (let TMP_808 \def (Bind b)
+in (let TMP_809 \def (CHead e TMP_808 u2) in (getl TMP_806 TMP_807
+TMP_809)))))) in (let TMP_811 \def (CTail k u1 x) in (let TMP_812 \def
+(refl_equal C TMP_811) in (let TMP_813 \def (Bind b) in (let TMP_814 \def
+(CHead x TMP_813 u2) in (let TMP_815 \def (getl_head k0 n c TMP_814 H5 t) in
+(let TMP_816 \def (ex_intro2 C TMP_805 TMP_810 x TMP_812 TMP_815) in (let
+TMP_817 \def (or_introl TMP_791 TMP_802 TMP_816) in (eq_ind_r C TMP_763
+TMP_782 TMP_817 c2 H4))))))))))))))))))))))))))))))))) in (ex2_ind C TMP_711
+TMP_715 TMP_734 TMP_818 H3)))))))))))))) in (let TMP_1084 \def (\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))))).(let TMP_822 \def (\lambda (_: nat).(let TMP_820 \def (r k0 n)
+in (let TMP_821 \def (clen c) in (eq nat TMP_820 TMP_821)))) in (let TMP_824
+\def (\lambda (_: nat).(let TMP_823 \def (Bind b) in (eq K k TMP_823))) in
+(let TMP_825 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_827 \def
+(\lambda (n0: nat).(let TMP_826 \def (CSort n0) in (eq C c2 TMP_826))) in
+(let TMP_829 \def (\lambda (e: C).(let TMP_828 \def (CTail k u1 e) in (eq C
+c2 TMP_828))) in (let TMP_834 \def (\lambda (e: C).(let TMP_830 \def (S n) in
+(let TMP_831 \def (CHead c k0 t) in (let TMP_832 \def (Bind b) in (let
+TMP_833 \def (CHead e TMP_832 u2) in (getl TMP_830 TMP_831 TMP_833)))))) in
+(let TMP_835 \def (ex2 C TMP_829 TMP_834) in (let TMP_839 \def (\lambda (_:
+nat).(let TMP_836 \def (S n) in (let TMP_837 \def (clen c) in (let TMP_838
+\def (s k0 TMP_837) in (eq nat TMP_836 TMP_838))))) in (let TMP_841 \def
+(\lambda (_: nat).(let TMP_840 \def (Bind b) in (eq K k TMP_840))) in (let
+TMP_842 \def (\lambda (_: nat).(eq T u1 u2)) in (let TMP_844 \def (\lambda
+(n0: nat).(let TMP_843 \def (CSort n0) in (eq C c2 TMP_843))) in (let TMP_845
+\def (ex4 nat TMP_839 TMP_841 TMP_842 TMP_844) in (let TMP_846 \def (or
+TMP_835 TMP_845) in (let TMP_1083 \def (\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 TMP_851 \def (\lambda (c0:
+C).(let TMP_847 \def (r k0 n) in (let TMP_848 \def (CTail k u1 c) in (let
+TMP_849 \def (Bind b) in (let TMP_850 \def (CHead c0 TMP_849 u2) in (getl
+TMP_847 TMP_848 TMP_850)))))) in (let TMP_852 \def (CTail k u1 c) in (let
+TMP_853 \def (Bind b) in (let TMP_854 \def (CHead c2 TMP_853 u2) in (let
+TMP_855 \def (getl_gen_S k0 TMP_852 TMP_854 t n H1) in (let TMP_856 \def
+(CSort x0) in (let H8 \def (eq_ind C c2 TMP_851 TMP_855 TMP_856 H7) in (let
+TMP_873 \def (\lambda (c0: C).((getl n (CHead (CTail k u1 c) k0 t) (CHead c0
+(Bind b) u2)) \to (let TMP_858 \def (\lambda (e: C).(let TMP_857 \def (CTail
+k u1 e) in (eq C c0 TMP_857))) in (let TMP_862 \def (\lambda (e: C).(let
+TMP_859 \def (CHead c k0 t) in (let TMP_860 \def (Bind b) in (let TMP_861
+\def (CHead e TMP_860 u2) in (getl n TMP_859 TMP_861))))) in (let TMP_863
+\def (ex2 C TMP_858 TMP_862) in (let TMP_866 \def (\lambda (_: nat).(let
+TMP_864 \def (clen c) in (let TMP_865 \def (s k0 TMP_864) in (eq nat n
+TMP_865)))) in (let TMP_868 \def (\lambda (_: nat).(let TMP_867 \def (Bind b)
+in (eq K k TMP_867))) in (let TMP_869 \def (\lambda (_: nat).(eq T u1 u2)) in
+(let TMP_871 \def (\lambda (n0: nat).(let TMP_870 \def (CSort n0) in (eq C c0
+TMP_870))) in (let TMP_872 \def (ex4 nat TMP_866 TMP_868 TMP_869 TMP_871) in
+(or TMP_863 TMP_872))))))))))) in (let TMP_874 \def (CSort x0) in (let H9
+\def (eq_ind C c2 TMP_873 H0 TMP_874 H7) in (let TMP_875 \def (CSort x0) in
+(let TMP_894 \def (\lambda (c0: C).(let TMP_877 \def (\lambda (e: C).(let
+TMP_876 \def (CTail k u1 e) in (eq C c0 TMP_876))) in (let TMP_882 \def
+(\lambda (e: C).(let TMP_878 \def (S n) in (let TMP_879 \def (CHead c k0 t)
+in (let TMP_880 \def (Bind b) in (let TMP_881 \def (CHead e TMP_880 u2) in
+(getl TMP_878 TMP_879 TMP_881)))))) in (let TMP_883 \def (ex2 C TMP_877
+TMP_882) in (let TMP_887 \def (\lambda (_: nat).(let TMP_884 \def (S n) in
+(let TMP_885 \def (clen c) in (let TMP_886 \def (s k0 TMP_885) in (eq nat
+TMP_884 TMP_886))))) in (let TMP_889 \def (\lambda (_: nat).(let TMP_888 \def
+(Bind b) in (eq K k TMP_888))) in (let TMP_890 \def (\lambda (_: nat).(eq T
+u1 u2)) in (let TMP_892 \def (\lambda (n0: nat).(let TMP_891 \def (CSort n0)
+in (eq C c0 TMP_891))) in (let TMP_893 \def (ex4 nat TMP_887 TMP_889 TMP_890
+TMP_892) in (or TMP_883 TMP_893)))))))))) in (let TMP_913 \def (\lambda (t0:
+T).((getl n (CHead (CTail k u1 c) k0 t) (CHead (CSort x0) (Bind b) t0)) \to
+(let TMP_897 \def (\lambda (e: C).(let TMP_895 \def (CSort x0) in (let
+TMP_896 \def (CTail k u1 e) in (eq C TMP_895 TMP_896)))) in (let TMP_901 \def
+(\lambda (e: C).(let TMP_898 \def (CHead c k0 t) in (let TMP_899 \def (Bind
+b) in (let TMP_900 \def (CHead e TMP_899 t0) in (getl n TMP_898 TMP_900)))))
+in (let TMP_902 \def (ex2 C TMP_897 TMP_901) in (let TMP_905 \def (\lambda
+(_: nat).(let TMP_903 \def (clen c) in (let TMP_904 \def (s k0 TMP_903) in
+(eq nat n TMP_904)))) in (let TMP_907 \def (\lambda (_: nat).(let TMP_906
+\def (Bind b) in (eq K k TMP_906))) in (let TMP_908 \def (\lambda (_:
+nat).(eq T u1 t0)) in (let TMP_911 \def (\lambda (n0: nat).(let TMP_909 \def
+(CSort x0) in (let TMP_910 \def (CSort n0) in (eq C TMP_909 TMP_910)))) in
+(let TMP_912 \def (ex4 nat TMP_905 TMP_907 TMP_908 TMP_911) in (or TMP_902
+TMP_912))))))))))) in (let H10 \def (eq_ind_r T u2 TMP_913 H9 u1 H6) in (let
+TMP_919 \def (\lambda (t0: T).(let TMP_914 \def (r k0 n) in (let TMP_915 \def
+(CTail k u1 c) in (let TMP_916 \def (CSort x0) in (let TMP_917 \def (Bind b)
+in (let TMP_918 \def (CHead TMP_916 TMP_917 t0) in (getl TMP_914 TMP_915
+TMP_918))))))) in (let H11 \def (eq_ind_r T u2 TMP_919 H8 u1 H6) in (let
+TMP_940 \def (\lambda (t0: T).(let TMP_922 \def (\lambda (e: C).(let TMP_920
+\def (CSort x0) in (let TMP_921 \def (CTail k u1 e) in (eq C TMP_920
+TMP_921)))) in (let TMP_927 \def (\lambda (e: C).(let TMP_923 \def (S n) in
+(let TMP_924 \def (CHead c k0 t) in (let TMP_925 \def (Bind b) in (let
+TMP_926 \def (CHead e TMP_925 t0) in (getl TMP_923 TMP_924 TMP_926)))))) in
+(let TMP_928 \def (ex2 C TMP_922 TMP_927) in (let TMP_932 \def (\lambda (_:
+nat).(let TMP_929 \def (S n) in (let TMP_930 \def (clen c) in (let TMP_931
+\def (s k0 TMP_930) in (eq nat TMP_929 TMP_931))))) in (let TMP_934 \def
+(\lambda (_: nat).(let TMP_933 \def (Bind b) in (eq K k TMP_933))) in (let
+TMP_935 \def (\lambda (_: nat).(eq T u1 t0)) in (let TMP_938 \def (\lambda
+(n0: nat).(let TMP_936 \def (CSort x0) in (let TMP_937 \def (CSort n0) in (eq
+C TMP_936 TMP_937)))) in (let TMP_939 \def (ex4 nat TMP_932 TMP_934 TMP_935
+TMP_938) in (or TMP_928 TMP_939)))))))))) in (let TMP_959 \def (\lambda (k1:
+K).((getl n (CHead (CTail k1 u1 c) k0 t) (CHead (CSort x0) (Bind b) u1)) \to
+(let TMP_943 \def (\lambda (e: C).(let TMP_941 \def (CSort x0) in (let
+TMP_942 \def (CTail k1 u1 e) in (eq C TMP_941 TMP_942)))) in (let TMP_947
+\def (\lambda (e: C).(let TMP_944 \def (CHead c k0 t) in (let TMP_945 \def
+(Bind b) in (let TMP_946 \def (CHead e TMP_945 u1) in (getl n TMP_944
+TMP_946))))) in (let TMP_948 \def (ex2 C TMP_943 TMP_947) in (let TMP_951
+\def (\lambda (_: nat).(let TMP_949 \def (clen c) in (let TMP_950 \def (s k0
+TMP_949) in (eq nat n TMP_950)))) in (let TMP_953 \def (\lambda (_: nat).(let
+TMP_952 \def (Bind b) in (eq K k1 TMP_952))) in (let TMP_954 \def (\lambda
+(_: nat).(eq T u1 u1)) in (let TMP_957 \def (\lambda (n0: nat).(let TMP_955
+\def (CSort x0) in (let TMP_956 \def (CSort n0) in (eq C TMP_955 TMP_956))))
+in (let TMP_958 \def (ex4 nat TMP_951 TMP_953 TMP_954 TMP_957) in (or TMP_948
+TMP_958))))))))))) in (let TMP_960 \def (Bind b) in (let H12 \def (eq_ind K k
+TMP_959 H10 TMP_960 H5) in (let TMP_966 \def (\lambda (k1: K).(let TMP_961
+\def (r k0 n) in (let TMP_962 \def (CTail k1 u1 c) in (let TMP_963 \def
+(CSort x0) in (let TMP_964 \def (Bind b) in (let TMP_965 \def (CHead TMP_963
+TMP_964 u1) in (getl TMP_961 TMP_962 TMP_965))))))) in (let TMP_967 \def
+(Bind b) in (let H13 \def (eq_ind K k TMP_966 H11 TMP_967 H5) in (let TMP_968
+\def (Bind b) in (let TMP_989 \def (\lambda (k1: K).(let TMP_971 \def
+(\lambda (e: C).(let TMP_969 \def (CSort x0) in (let TMP_970 \def (CTail k1
+u1 e) in (eq C TMP_969 TMP_970)))) in (let TMP_976 \def (\lambda (e: C).(let
+TMP_972 \def (S n) in (let TMP_973 \def (CHead c k0 t) in (let TMP_974 \def
+(Bind b) in (let TMP_975 \def (CHead e TMP_974 u1) in (getl TMP_972 TMP_973
+TMP_975)))))) in (let TMP_977 \def (ex2 C TMP_971 TMP_976) in (let TMP_981
+\def (\lambda (_: nat).(let TMP_978 \def (S n) in (let TMP_979 \def (clen c)
+in (let TMP_980 \def (s k0 TMP_979) in (eq nat TMP_978 TMP_980))))) in (let
+TMP_983 \def (\lambda (_: nat).(let TMP_982 \def (Bind b) in (eq K k1
+TMP_982))) in (let TMP_984 \def (\lambda (_: nat).(eq T u1 u1)) in (let
+TMP_987 \def (\lambda (n0: nat).(let TMP_985 \def (CSort x0) in (let TMP_986
+\def (CSort n0) in (eq C TMP_985 TMP_986)))) in (let TMP_988 \def (ex4 nat
+TMP_981 TMP_983 TMP_984 TMP_987) in (or TMP_977 TMP_988)))))))))) in (let
+TMP_990 \def (r k0 n) in (let TMP_1012 \def (\lambda (n0: nat).(let TMP_994
+\def (\lambda (e: C).(let TMP_991 \def (CSort x0) in (let TMP_992 \def (Bind
+b) in (let TMP_993 \def (CTail TMP_992 u1 e) in (eq C TMP_991 TMP_993))))) in
+(let TMP_999 \def (\lambda (e: C).(let TMP_995 \def (S n) in (let TMP_996
+\def (CHead c k0 t) in (let TMP_997 \def (Bind b) in (let TMP_998 \def (CHead
+e TMP_997 u1) in (getl TMP_995 TMP_996 TMP_998)))))) in (let TMP_1000 \def
+(ex2 C TMP_994 TMP_999) in (let TMP_1003 \def (\lambda (_: nat).(let TMP_1001
+\def (S n) in (let TMP_1002 \def (s k0 n0) in (eq nat TMP_1001 TMP_1002))))
+in (let TMP_1006 \def (\lambda (_: nat).(let TMP_1004 \def (Bind b) in (let
+TMP_1005 \def (Bind b) in (eq K TMP_1004 TMP_1005)))) in (let TMP_1007 \def
+(\lambda (_: nat).(eq T u1 u1)) in (let TMP_1010 \def (\lambda (n1: nat).(let
+TMP_1008 \def (CSort x0) in (let TMP_1009 \def (CSort n1) in (eq C TMP_1008
+TMP_1009)))) in (let TMP_1011 \def (ex4 nat TMP_1003 TMP_1006 TMP_1007
+TMP_1010) in (or TMP_1000 TMP_1011)))))))))) in (let TMP_1013 \def (S n) in
+(let TMP_1034 \def (\lambda (n0: nat).(let TMP_1017 \def (\lambda (e: C).(let
+TMP_1014 \def (CSort x0) in (let TMP_1015 \def (Bind b) in (let TMP_1016 \def
+(CTail TMP_1015 u1 e) in (eq C TMP_1014 TMP_1016))))) in (let TMP_1022 \def
+(\lambda (e: C).(let TMP_1018 \def (S n) in (let TMP_1019 \def (CHead c k0 t)
+in (let TMP_1020 \def (Bind b) in (let TMP_1021 \def (CHead e TMP_1020 u1) in
+(getl TMP_1018 TMP_1019 TMP_1021)))))) in (let TMP_1023 \def (ex2 C TMP_1017
+TMP_1022) in (let TMP_1025 \def (\lambda (_: nat).(let TMP_1024 \def (S n) in
+(eq nat TMP_1024 n0))) in (let TMP_1028 \def (\lambda (_: nat).(let TMP_1026
+\def (Bind b) in (let TMP_1027 \def (Bind b) in (eq K TMP_1026 TMP_1027))))
+in (let TMP_1029 \def (\lambda (_: nat).(eq T u1 u1)) in (let TMP_1032 \def
+(\lambda (n1: nat).(let TMP_1030 \def (CSort x0) in (let TMP_1031 \def (CSort
+n1) in (eq C TMP_1030 TMP_1031)))) in (let TMP_1033 \def (ex4 nat TMP_1025
+TMP_1028 TMP_1029 TMP_1032) in (or TMP_1023 TMP_1033)))))))))) in (let
+TMP_1038 \def (\lambda (e: C).(let TMP_1035 \def (CSort x0) in (let TMP_1036
+\def (Bind b) in (let TMP_1037 \def (CTail TMP_1036 u1 e) in (eq C TMP_1035
+TMP_1037))))) in (let TMP_1043 \def (\lambda (e: C).(let TMP_1039 \def (S n)
+in (let TMP_1040 \def (CHead c k0 t) in (let TMP_1041 \def (Bind b) in (let
+TMP_1042 \def (CHead e TMP_1041 u1) in (getl TMP_1039 TMP_1040 TMP_1042))))))
+in (let TMP_1044 \def (ex2 C TMP_1038 TMP_1043) in (let TMP_1047 \def
+(\lambda (_: nat).(let TMP_1045 \def (S n) in (let TMP_1046 \def (S n) in (eq
+nat TMP_1045 TMP_1046)))) in (let TMP_1050 \def (\lambda (_: nat).(let
+TMP_1048 \def (Bind b) in (let TMP_1049 \def (Bind b) in (eq K TMP_1048
+TMP_1049)))) in (let TMP_1051 \def (\lambda (_: nat).(eq T u1 u1)) in (let
+TMP_1054 \def (\lambda (n0: nat).(let TMP_1052 \def (CSort x0) in (let
+TMP_1053 \def (CSort n0) in (eq C TMP_1052 TMP_1053)))) in (let TMP_1055 \def
+(ex4 nat TMP_1047 TMP_1050 TMP_1051 TMP_1054) in (let TMP_1058 \def (\lambda
+(_: nat).(let TMP_1056 \def (S n) in (let TMP_1057 \def (S n) in (eq nat
+TMP_1056 TMP_1057)))) in (let TMP_1061 \def (\lambda (_: nat).(let TMP_1059
+\def (Bind b) in (let TMP_1060 \def (Bind b) in (eq K TMP_1059 TMP_1060))))
+in (let TMP_1062 \def (\lambda (_: nat).(eq T u1 u1)) in (let TMP_1065 \def
+(\lambda (n0: nat).(let TMP_1063 \def (CSort x0) in (let TMP_1064 \def (CSort
+n0) in (eq C TMP_1063 TMP_1064)))) in (let TMP_1066 \def (S n) in (let
+TMP_1067 \def (refl_equal nat TMP_1066) in (let TMP_1068 \def (Bind b) in
+(let TMP_1069 \def (refl_equal K TMP_1068) in (let TMP_1070 \def (refl_equal
+T u1) in (let TMP_1071 \def (CSort x0) in (let TMP_1072 \def (refl_equal C
+TMP_1071) in (let TMP_1073 \def (ex4_intro nat TMP_1058 TMP_1061 TMP_1062
+TMP_1065 x0 TMP_1067 TMP_1069 TMP_1070 TMP_1072) in (let TMP_1074 \def
+(or_intror TMP_1044 TMP_1055 TMP_1073) in (let TMP_1075 \def (r k0 n) in (let
+TMP_1076 \def (s k0 TMP_1075) in (let TMP_1077 \def (s_r k0 n) in (let
+TMP_1078 \def (eq_ind_r nat TMP_1013 TMP_1034 TMP_1074 TMP_1076 TMP_1077) in
+(let TMP_1079 \def (clen c) in (let TMP_1080 \def (eq_ind nat TMP_990
+TMP_1012 TMP_1078 TMP_1079 H4) in (let TMP_1081 \def (eq_ind_r K TMP_968
+TMP_989 TMP_1080 k H5) in (let TMP_1082 \def (eq_ind T u1 TMP_940 TMP_1081 u2
+H6) in (eq_ind_r C TMP_875 TMP_894 TMP_1082 c2
+H7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
+(ex4_ind nat TMP_822 TMP_824 TMP_825 TMP_827 TMP_846 TMP_1083
+H3)))))))))))))))) in (or_ind TMP_681 TMP_690 TMP_709 TMP_819 TMP_1084
+H2)))))))))))))))))))))))))))))) in (nat_ind TMP_245 TMP_669 TMP_1085
+i))))))))) in (C_ind TMP_15 TMP_228 TMP_1086 c1))))))))).