-(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
+(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