-(c0: C).(drop h d c0 e)) H0 a (drop_gen_refl c a H)) in (let H3 \def (match
-H1 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to
-(drop (minus O h) O e a)))) with [le_n \Rightarrow (\lambda (H3: (eq nat
-(plus d h) O)).(let H4 \def (f_equal nat nat (\lambda (e0: nat).e0) (plus d
-h) O H3) in (eq_ind nat (plus d h) (\lambda (n: nat).(drop (minus n h) n e
-a)) (eq_ind_r nat O (\lambda (n: nat).(drop (minus n h) n e a)) (and_ind (eq
-nat d O) (eq nat h O) (drop O O e a) (\lambda (H5: (eq nat d O)).(\lambda
-(H6: (eq nat h O)).(let H7 \def (eq_ind nat d (\lambda (n: nat).(drop h n a
-e)) H2 O H5) in (let H8 \def (eq_ind nat h (\lambda (n: nat).(drop n O a e))
-H7 O H6) in (eq_ind C a (\lambda (c0: C).(drop O O c0 a)) (drop_refl a) e
-(drop_gen_refl a e H8)))))) (plus_O d h H4)) (plus d h) H4) O H4))) | (le_S m
-H3) \Rightarrow (\lambda (H4: (eq nat (S m) O)).((let H5 \def (eq_ind nat (S
-m) (\lambda (e0: nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind ((le
-(plus d h) m) \to (drop (minus O h) O e a)) H5)) H3))]) in (H3 (refl_equal
-nat O)))))))))))) (\lambda (i0: nat).(\lambda (H: ((\forall (a: C).(\forall
-(c: C).((drop i0 O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
-nat).((drop h d c e) \to ((le (plus d h) i0) \to (drop (minus i0 h) O e
-a))))))))))).(\lambda (a: C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop
-(S i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop
-h d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
-a)))))))) (\lambda (n: nat).(\lambda (H0: (drop (S i0) O (CSort n)
-a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (drop h
-d (CSort n) e)).(\lambda (H2: (le (plus d h) (S i0))).(and3_ind (eq C e
-(CSort n)) (eq nat h O) (eq nat d O) (drop (minus (S i0) h) O e a) (\lambda
-(H3: (eq C e (CSort n))).(\lambda (H4: (eq nat h O)).(\lambda (H5: (eq nat d
-O)).(and3_ind (eq C a (CSort n)) (eq nat (S i0) O) (eq nat O O) (drop (minus
-(S i0) h) O e a) (\lambda (H6: (eq C a (CSort n))).(\lambda (H7: (eq nat (S
-i0) O)).(\lambda (_: (eq nat O O)).(let H9 \def (eq_ind nat d (\lambda (n0:
-nat).(le (plus n0 h) (S i0))) H2 O H5) in (let H10 \def (eq_ind nat h
-(\lambda (n0: nat).(le (plus O n0) (S i0))) H9 O H4) in (eq_ind_r nat O
-(\lambda (n0: nat).(drop (minus (S i0) n0) O e a)) (eq_ind_r C (CSort n)
-(\lambda (c0: C).(drop (minus (S i0) O) O c0 a)) (eq_ind_r C (CSort n)
-(\lambda (c0: C).(drop (minus (S i0) O) O (CSort n) c0)) (let H11 \def
-(eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat return (\lambda (_:
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7) in
-(False_ind (drop (minus (S i0) O) O (CSort n) (CSort n)) H11)) a H6) e H3) h
-H4)))))) (drop_gen_sort n (S i0) O a H0))))) (drop_gen_sort n h d e
-H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S i0) O c0 a) \to
-(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le
-(plus d h) (S i0)) \to (drop (minus (S i0) h) O e a))))))))).(\lambda (k:
-K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S i0) O (CHead c0 k0 t) a)
-\to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d (CHead c0
-k0 t) e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
-a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1: (drop (S i0) O
-(CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
-nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t) e)).(\lambda (H3: (le
-(plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Bind b)
-t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S i0) h) O e a))))
-(\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus O
-h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 (Bind b) t) e)
-\to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda
-(H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le (plus O O) (S
-i0))).(eq_ind C (CHead c0 (Bind b) t) (\lambda (c1: C).(drop (minus (S i0) O)
-O c1 a)) (drop_drop (Bind b) i0 c0 a (drop_gen_drop (Bind b) c0 a t i0 H1) t)
-e (drop_gen_refl (CHead c0 (Bind b) t) e H6)))) (\lambda (h0: nat).(\lambda
-(_: (((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O h0) (S i0)) \to
-(drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0) O (CHead c0
-(Bind b) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H a c0
-(drop_gen_drop (Bind b) c0 a t i0 H1) e h0 O (drop_gen_drop (Bind b) c0 e t
-h0 H6) (le_S_n (plus O h0) i0 H7)))))) h H4 H5))) (\lambda (d0: nat).(\lambda
-(_: (((drop h d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h) (S i0)) \to
-(drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0) (CHead c0
-(Bind b) t) e)).(\lambda (H5: (le (plus (S d0) h) (S i0))).(ex3_2_ind C T
-(\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Bind b) v)))) (\lambda
-(_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0) v)))) (\lambda (e0:
-C).(\lambda (_: T).(drop h (r (Bind b) d0) c0 e0))) (drop (minus (S i0) h) O
-e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C e (CHead x0 (Bind
-b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) d0) x1))).(\lambda (H8:
-(drop h (r (Bind b) d0) c0 x0)).(eq_ind_r C (CHead x0 (Bind b) x1) (\lambda
-(c1: C).(drop (minus (S i0) h) O c1 a)) (eq_ind nat (S (minus i0 h)) (\lambda
-(n: nat).(drop n O (CHead x0 (Bind b) x1) a)) (drop_drop (Bind b) (minus i0
-h) x0 a (H a c0 (drop_gen_drop (Bind b) c0 a t i0 H1) x0 h d0 H8 (le_S_n
-(plus d0 h) i0 H5)) x1) (minus (S i0) h) (minus_Sn_m i0 h (le_trans_plus_r d0
-h i0 (le_S_n (plus d0 h) i0 H5)))) e H6)))))) (drop_gen_skip_l c0 e t h d0
-(Bind b) H4)))))) d H2 H3))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda
-(H1: (drop (S i0) O (CHead c0 (Flat f) t) a)).(\lambda (e: C).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Flat f) t)
+(c0: C).(drop h d c0 e)) H0 a (drop_gen_refl c a H)) in (let H_y \def
+(le_n_O_eq (plus d h) H1) in (land_ind (eq nat d O) (eq nat h O) (drop (minus
+O h) O e a) (\lambda (H3: (eq nat d O)).(\lambda (H4: (eq nat h O)).(let H5
+\def (eq_ind nat d (\lambda (n: nat).(drop h n a e)) H2 O H3) in (let H6 \def
+(eq_ind nat h (\lambda (n: nat).(drop n O a e)) H5 O H4) in (eq_ind_r nat O
+(\lambda (n: nat).(drop (minus O n) O e a)) (eq_ind C a (\lambda (c0:
+C).(drop (minus O O) O c0 a)) (drop_refl a) e (drop_gen_refl a e H6)) h
+H4))))) (plus_O d h (sym_eq nat O (plus d h) H_y))))))))))))) (\lambda (i0:
+nat).(\lambda (H: ((\forall (a: C).(\forall (c: C).((drop i0 O c a) \to
+(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
+(plus d h) i0) \to (drop (minus i0 h) O e a))))))))))).(\lambda (a:
+C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop (S i0) O c0 a) \to (\forall
+(e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d
+h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))) (\lambda (n:
+nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda (H2:
+(le (plus d h) (S i0))).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat d
+O) (drop (minus (S i0) h) O e a) (\lambda (H3: (eq C e (CSort n))).(\lambda
+(H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(and3_ind (eq C a (CSort n))
+(eq nat (S i0) O) (eq nat O O) (drop (minus (S i0) h) O e a) (\lambda (H6:
+(eq C a (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O
+O)).(let H9 \def (eq_ind nat d (\lambda (n0: nat).(le (plus n0 h) (S i0))) H2
+O H5) in (let H10 \def (eq_ind nat h (\lambda (n0: nat).(le (plus O n0) (S
+i0))) H9 O H4) in (eq_ind_r nat O (\lambda (n0: nat).(drop (minus (S i0) n0)
+O e a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O c0
+a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O (CSort n)
+c0)) (let H11 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat
+return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H7) in (False_ind (drop (minus (S i0) O) O (CSort n) (CSort n))
+H11)) a H6) e H3) h H4)))))) (drop_gen_sort n (S i0) O a H0)))))
+(drop_gen_sort n h d e H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S
+i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
+d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
+a))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S
+i0) O (CHead c0 k0 t) a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
+nat).((drop h d (CHead c0 k0 t) e) \to ((le (plus d h) (S i0)) \to (drop
+(minus (S i0) h) O e a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1:
+(drop (S i0) O (CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t)