-O O)).(let H3 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee in nat
-return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
-True])) I O H1) in (False_ind (ex2_3 B C T (\lambda (b: B).(\lambda (e:
-C).(\lambda (v: T).(clear (CSort n) (CHead e (Bind b) v))))) (\lambda (_:
-B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))) H3))))) (drop_gen_sort
-n (S i) O c2 H)))))) (\lambda (c: C).(\lambda (H: ((\forall (c2: C).(\forall
-(i: nat).((drop (S i) O c c2) \to (ex2_3 B C T (\lambda (b: B).(\lambda (e:
-C).(\lambda (v: T).(clear c (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda
-(e: C).(\lambda (_: T).(drop i O e c2)))))))))).(\lambda (k: K).(\lambda (t:
-T).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop (S i) O (CHead c k
-t) c2)).(K_ind (\lambda (k0: K).((drop (r k0 i) O c c2) \to (ex2_3 B C T
-(\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear (CHead c k0 t) (CHead
-e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e
-c2))))))) (\lambda (b: B).(\lambda (H1: (drop (r (Bind b) i) O c
-c2)).(ex2_3_intro B C T (\lambda (b0: B).(\lambda (e: C).(\lambda (v:
-T).(clear (CHead c (Bind b) t) (CHead e (Bind b0) v))))) (\lambda (_:
-B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) b c t (clear_bind b c
-t) H1))) (\lambda (f: F).(\lambda (H1: (drop (r (Flat f) i) O c c2)).(let H2
-\def (H c2 i H1) in (ex2_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda
-(v: T).(clear c (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e:
-C).(\lambda (_: T).(drop i O e c2)))) (ex2_3 B C T (\lambda (b: B).(\lambda
-(e: C).(\lambda (v: T).(clear (CHead c (Flat f) t) (CHead e (Bind b) v)))))
-(\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))) (\lambda
-(x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H3: (clear c (CHead x1
-(Bind x0) x2))).(\lambda (H4: (drop i O x1 c2)).(ex2_3_intro B C T (\lambda
-(b: B).(\lambda (e: C).(\lambda (v: T).(clear (CHead c (Flat f) t) (CHead e