LambdaDelta.ma and some slices of it that typecheck ok!

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta-5.ma

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta-5".

include "LambdaDelta-4.ma".

inductive drop: nat \to (nat \to (C \to (C \to Prop))) \def
| drop_refl: \forall (c: C).(drop O O c c)
| drop_drop: \forall (k: K).(\forall (h: nat).(\forall (c: C).(\forall (e: C).((drop (r k h) O c e) \to (\forall (u: T).(drop (S h) O (CHead c k u) e))))))
| drop_skip: \forall (k: K).(\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h (r k d) c e) \to (\forall (u: T).(drop h (S d) (CHead c k (lift h (r k d) u)) (CHead e k u)))))))).

theorem drop_gen_sort:
 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(\forall (x: C).((drop h d (CSort n) x) \to (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O))))))
\def
 \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (x: C).(\lambda (H: (drop h d (CSort n) x)).(insert_eq C (CSort n) (\lambda (c: C).(drop h d c x)) (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O)) (\lambda (y: C).(\lambda (H0: (drop h d y x)).(drop_ind (\lambda (n0: nat).(\lambda (n1: nat).(\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n)) \to (and3 (eq C c0 (CSort n)) (eq nat n0 O) (eq nat n1 O))))))) (\lambda (c: C).(\lambda (H1: (eq C c (CSort n))).(let H2 \def (f_equal C C (\lambda (e: C).e) c (CSort n) H1) in (eq_ind_r C (CSort n) (\lambda (c0: C).(and3 (eq C c0 (CSort n)) (eq nat O O) (eq nat O O))) (and3_intro (eq C (CSort n) (CSort n)) (eq nat O O) (eq nat O O) (refl_equal C (CSort n)) (refl_equal nat O) (refl_equal nat O)) c H2)))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (c: C).(\lambda (e: C).(\lambda (_: (drop (r k h0) O c e)).(\lambda (_: (((eq C c (CSort n)) \to (and3 (eq C e (CSort n)) (eq nat (r k h0) O) (eq nat O O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k u) (CSort n))).(let H4 \def (eq_ind C (CHead c k u) (\lambda (ee: C).(match ee return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (and3 (eq C e (CSort n)) (eq nat (S h0) O) (eq nat O O)) H4)))))))))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (d0: nat).(\lambda (c: C).(\lambda (e: C).(\lambda (_: (drop h0 (r k d0) c e)).(\lambda (_: (((eq C c (CSort n)) \to (and3 (eq C e (CSort n)) (eq nat h0 O) (eq nat (r k d0) O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k (lift h0 (r k d0) u)) (CSort n))).(let H4 \def (eq_ind C (CHead c k (lift h0 (r k d0) u)) (\lambda (ee: C).(match ee return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (and3 (eq C (CHead e k u) (CSort n)) (eq nat h0 O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) H))))).

theorem drop_gen_refl:
 \forall (x: C).(\forall (e: C).((drop O O x e) \to (eq C x e)))
\def
 \lambda (x: C).(\lambda (e: C).(\lambda (H: (drop O O x e)).(insert_eq nat O (\lambda (n: nat).(drop n O x e)) (eq C x e) (\lambda (y: nat).(\lambda (H0: (drop y O x e)).(insert_eq nat O (\lambda (n: nat).(drop y n x e)) ((eq nat y O) \to (eq C x e)) (\lambda (y0: nat).(\lambda (H1: (drop y y0 x e)).(drop_ind (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c: C).(\lambda (c0: C).((eq nat n0 O) \to ((eq nat n O) \to (eq C c c0))))))) (\lambda (c: C).(\lambda (_: (eq nat O O)).(\lambda (_: (eq nat O O)).(refl_equal C c)))) (\lambda (k: K).(\lambda (h: nat).(\lambda (c: C).(\lambda (e0: C).(\lambda (_: (drop (r k h) O c e0)).(\lambda (_: (((eq nat O O) \to ((eq nat (r k h) O) \to (eq C c e0))))).(\lambda (u: T).(\lambda (_: (eq nat O O)).(\lambda (H5: (eq nat (S h) O)).(let H6 \def (eq_ind nat (S h) (\lambda (ee: nat).(match ee return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H5) in (False_ind (eq C (CHead c k u) e0) H6))))))))))) (\lambda (k: K).(\lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e0: C).(\lambda (H2: (drop h (r k d) c e0)).(\lambda (H3: (((eq nat (r k d) O) \to ((eq nat h O) \to (eq C c e0))))).(\lambda (u: T).(\lambda (H4: (eq nat (S d) O)).(\lambda (H5: (eq nat h O)).(let H6 \def (f_equal nat nat (\lambda (e1: nat).e1) h O H5) in (let H7 \def (eq_ind nat h (\lambda (n: nat).((eq nat (r k d) O) \to ((eq nat n O) \to (eq C c e0)))) H3 O H6) in (let H8 \def (eq_ind nat h (\lambda (n: nat).(drop n (r k d) c e0)) H2 O H6) in (eq_ind_r nat O (\lambda (n: nat).(eq C (CHead c k (lift n (r k d) u)) (CHead e0 k u))) (let H9 \def (eq_ind nat (S d) (\lambda (ee: nat).(match ee return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind (eq C (CHead c k (lift O (r k d) u)) (CHead e0 k u)) H9)) h H6)))))))))))))) y y0 x e H1))) H0))) H))).

theorem drop_gen_drop:
 \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).((drop (S h) O (CHead c k u) x) \to (drop (r k h) O c x))))))
\def
 \lambda (k: K).(\lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda (H: (drop (S h) O (CHead c k u) x)).(insert_eq C (CHead c k u) (\lambda (c0: C).(drop (S h) O c0 x)) (drop (r k h) O c x) (\lambda (y: C).(\lambda (H0: (drop (S h) O y x)).(insert_eq nat O (\lambda (n: nat).(drop (S h) n y x)) ((eq C y (CHead c k u)) \to (drop (r k h) O c x)) (\lambda (y0: nat).(\lambda (H1: (drop (S h) y0 y x)).(insert_eq nat (S h) (\lambda (n: nat).(drop n y0 y x)) ((eq nat y0 O) \to ((eq C y (CHead c k u)) \to (drop (r k h) O c x))) (\lambda (y1: nat).(\lambda (H2: (drop y1 y0 y x)).(drop_ind (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq nat n (S h)) \to ((eq nat n0 O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) O c c1)))))))) (\lambda (c0: C).(\lambda (H3: (eq nat O (S h))).(\lambda (_: (eq nat O O)).(\lambda (_: (eq C c0 (CHead c k u))).(let H6 \def (match H3 return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n (S h)) \to (drop (r k h) O c c0)))) with [refl_equal \Rightarrow (\lambda (H2: (eq nat O (S h))).(let H3 \def (eq_ind nat O (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S h) H2) in (False_ind (drop (r k h) O c c0) H3)))]) in (H6 (refl_equal nat (S h)))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (H3: (drop (r k0 h0) O c0 e)).(\lambda (_: (((eq nat (r k0 h0) (S h)) \to ((eq nat O O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) O c e)))))).(\lambda (u0: T).(\lambda (H5: (eq nat (S h0) (S h))).(\lambda (_: (eq nat O O)).(\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c k u))).(let H8 \def (match H5 return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n (S h)) \to (drop (r k h) O c e)))) with [refl_equal \Rightarrow (\lambda (H4: (eq nat (S h0) (S h))).(let H5 \def (f_equal nat nat (\lambda (e0: nat).(match e0 return (\lambda (_: nat).nat) with [O \Rightarrow h0 | (S n) \Rightarrow n])) (S h0) (S h) H4) in (eq_ind nat h (\lambda (_: nat).(drop (r k h) O c e)) (let H6 \def (match H7 return (\lambda (c0: C).(\lambda (_: (eq ? ? c0)).((eq C c0 (CHead c k u)) \to (drop (r k h) O c e)))) with [refl_equal \Rightarrow (\lambda (H4: (eq C (CHead c0 k0 u0) (CHead c k u))).(let H6 \def (f_equal C T (\lambda (e0: C).(match e0 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 u0) (CHead c k u) H4) in ((let H7 \def (f_equal C K (\lambda (e0: C).(match e0 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k _) \Rightarrow k])) (CHead c0 k0 u0) (CHead c k u) H4) in ((let H8 \def (f_equal C C (\lambda (e0: C).(match e0 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k0 u0) (CHead c k u) H4) in (eq_ind C c (\lambda (_: C).((eq K k0 k) \to ((eq T u0 u) \to (drop (r k h) O c e)))) (\lambda (H9: (eq K k0 k)).(eq_ind K k (\lambda (_: K).((eq T u0 u) \to (drop (r k h) O c e))) (\lambda (H10: (eq T u0 u)).(eq_ind T u (\lambda (_: T).(drop (r k h) O c e)) (eq_ind nat h0 (\lambda (n: nat).(drop (r k n) O c e)) (eq_ind C c0 (\lambda (c: C).(drop (r k h0) O c e)) (eq_ind K k0 (\lambda (k: K).(drop (r k h0) O c0 e)) H3 k H9) c H8) h H5) u0 (sym_eq T u0 u H10))) k0 (sym_eq K k0 k H9))) c0 (sym_eq C c0 c H8))) H7)) H6)))]) in (H6 (refl_equal C (CHead c k u)))) h0 (sym_eq nat h0 h H5))))]) in (H8 (refl_equal nat (S h)))))))))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda (d: nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (_: (drop h0 (r k0 d) c0 e)).(\lambda (_: (((eq nat h0 (S h)) \to ((eq nat (r k0 d) O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) O c e)))))).(\lambda (u0: T).(\lambda (_: (eq nat h0 (S h))).(\lambda (H6: (eq nat (S d) O)).(\lambda (_: (eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k u))).(let H8 \def (match H6 return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n O) \to (drop (r k h) O c (CHead e k0 u0))))) with [refl_equal \Rightarrow (\lambda (H4: (eq nat (S d) O)).(let H5 \def (eq_ind nat (S d) (\lambda (e0: nat).(match e0 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind (drop (r k h) O c (CHead e k0 u0)) H5)))]) in (H8 (refl_equal nat O)))))))))))))) y1 y0 y x H2))) H1))) H0))) H)))))).

theorem drop_gen_skip_r:
 \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall (d: nat).(\forall (k: K).((drop h (S d) x (CHead c k u)) \to (ex2 C (\lambda (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e: C).(drop h (r k d) e c)))))))))
\def
 \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) x (CHead c k u))).(let H0 \def (match H return (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (drop n n0 c0 c1)).((eq nat n h) \to ((eq nat n0 (S d)) \to ((eq C c0 x) \to ((eq C c1 (CHead c k u)) \to (ex2 C (\lambda (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e: C).(drop h (r k d) e c)))))))))))) with [(drop_refl c0) \Rightarrow (\lambda (H0: (eq nat O h)).(\lambda (H1: (eq nat O (S d))).(\lambda (H2: (eq C c0 x)).(\lambda (H3: (eq C c0 (CHead c k u))).(eq_ind nat O (\lambda (n: nat).((eq nat O (S d)) \to ((eq C c0 x) \to ((eq C c0 (CHead c k u)) \to (ex2 C (\lambda (e: C).(eq C x (CHead e k (lift n (r k d) u)))) (\lambda (e: C).(drop n (r k d) e c))))))) (\lambda (H4: (eq nat O (S d))).(let H5 \def (eq_ind nat O (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4) in (False_ind ((eq C c0 x) \to ((eq C c0 (CHead c k u)) \to (ex2 C (\lambda (e: C).(eq C x (CHead e k (lift O (r k d) u)))) (\lambda (e: C).(drop O (r k d) e c))))) H5))) h H0 H1 H2 H3))))) | (drop_drop k0 h0 c0 e H0 u0) \Rightarrow (\lambda (H1: (eq nat (S h0) h)).(\lambda (H2: (eq nat O (S d))).(\lambda (H3: (eq C (CHead c0 k0 u0) x)).(\lambda (H4: (eq C e (CHead c k u))).(eq_ind nat (S h0) (\lambda (n: nat).((eq nat O (S d)) \to ((eq C (CHead c0 k0 u0) x) \to ((eq C e (CHead c k u)) \to ((drop (r k0 h0) O c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift n (r k d) u)))) (\lambda (e0: C).(drop n (r k d) e0 c)))))))) (\lambda (H5: (eq nat O (S d))).(let H6 \def (eq_ind nat O (\lambda (e0: nat).(match e0 return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H5) in (False_ind ((eq C (CHead c0 k0 u0) x) \to ((eq C e (CHead c k u)) \to ((drop (r k0 h0) O c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift (S h0) (r k d) u)))) (\lambda (e0: C).(drop (S h0) (r k d) e0 c)))))) H6))) h H1 H2 H3 H4 H0))))) | (drop_skip k0 h0 d0 c0 e H0 u0) \Rightarrow (\lambda (H1: (eq nat h0 h)).(\lambda (H2: (eq nat (S d0) (S d))).(\lambda (H3: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) x)).(\lambda (H4: (eq C (CHead e k0 u0) (CHead c k u))).(eq_ind nat h (\lambda (n: nat).((eq nat (S d0) (S d)) \to ((eq C (CHead c0 k0 (lift n (r k0 d0) u0)) x) \to ((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop n (r k0 d0) c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c)))))))) (\lambda (H5: (eq nat (S d0) (S d))).(let H6 \def (f_equal nat nat (\lambda (e0: nat).(match e0 return (\lambda (_: nat).nat) with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0) (S d) H5) in (eq_ind nat d (\lambda (n: nat).((eq C (CHead c0 k0 (lift h (r k0 n) u0)) x) \to ((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop h (r k0 n) c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c))))))) (\lambda (H7: (eq C (CHead c0 k0 (lift h (r k0 d) u0)) x)).(eq_ind C (CHead c0 k0 (lift h (r k0 d) u0)) (\lambda (c1: C).((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop h (r k0 d) c0 e) \to (ex2 C (\lambda (e0: C).(eq C c1 (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c)))))) (\lambda (H8: (eq C (CHead e k0 u0) (CHead c k u))).(let H9 \def (f_equal C T (\lambda (e0: C).(match e0 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e k0 u0) (CHead c k u) H8) in ((let H10 \def (f_equal C K (\lambda (e0: C).(match e0 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k _) \Rightarrow k])) (CHead e k0 u0) (CHead c k u) H8) in ((let H11 \def (f_equal C C (\lambda (e0: C).(match e0 return (\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c _ _) \Rightarrow c])) (CHead e k0 u0) (CHead c k u) H8) in (eq_ind C c (\lambda (c1: C).((eq K k0 k) \to ((eq T u0 u) \to ((drop h (r k0 d) c0 c1) \to (ex2 C (\lambda (e0: C).(eq C (CHead c0 k0 (lift h (r k0 d) u0)) (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c))))))) (\lambda (H12: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T u0 u) \to ((drop h (r k1 d) c0 c) \to (ex2 C (\lambda (e0: C).(eq C (CHead c0 k1 (lift h (r k1 d) u0)) (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c)))))) (\lambda (H13: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((drop h (r k d) c0 c) \to (ex2 C (\lambda (e0: C).(eq C (CHead c0 k (lift h (r k d) t)) (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c))))) (\lambda (H14: (drop h (r k d) c0 c)).(let H15 \def (eq_ind T u0 (\lambda (t: T).(eq C (CHead c0 k0 (lift h (r k0 d) t)) x)) H7 u H13) in (let H16 \def (eq_ind K k0 (\lambda (k: K).(eq C (CHead c0 k (lift h (r k d) u)) x)) H15 k H12) in (let H17 \def (eq_ind_r C x (\lambda (c0: C).(drop h (S d) c0 (CHead c k u))) H (CHead c0 k (lift h (r k d) u)) H16) in (ex_intro2 C (\lambda (e0: C).(eq C (CHead c0 k (lift h (r k d) u)) (CHead e0 k (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c)) c0 (refl_equal C (CHead c0 k (lift h (r k d) u))) H14))))) u0 (sym_eq T u0 u H13))) k0 (sym_eq K k0 k H12))) e (sym_eq C e c H11))) H10)) H9))) x H7)) d0 (sym_eq nat d0 d H6)))) h0 (sym_eq nat h0 h H1) H2 H3 H4 H0)))))]) in (H0 (refl_equal nat h) (refl_equal nat (S d)) (refl_equal C x) (refl_equal C (CHead c k u)))))))))).

theorem drop_gen_skip_l:
 \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall (d: nat).(\forall (k: K).((drop h (S d) (CHead c k u) x) \to (ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k d) c e))))))))))
\def
 \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) (CHead c k u) x)).(let H0 \def (match H return (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (drop n n0 c0 c1)).((eq nat n h) \to ((eq nat n0 (S d)) \to ((eq C c0 (CHead c k u)) \to ((eq C c1 x) \to (ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k d) c e))))))))))))) with [(drop_refl c0) \Rightarrow (\lambda (H0: (eq nat O h)).(\lambda (H1: (eq nat O (S d))).(\lambda (H2: (eq C c0 (CHead c k u))).(\lambda (H3: (eq C c0 x)).(eq_ind nat O (\lambda (n: nat).((eq nat O (S d)) \to ((eq C c0 (CHead c k u)) \to ((eq C c0 x) \to (ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift n (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop n (r k d) c e)))))))) (\lambda (H4: (eq nat O (S d))).(let H5 \def (eq_ind nat O (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4) in (False_ind ((eq C c0 (CHead c k u)) \to ((eq C c0 x) \to (ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift O (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop O (r k d) c e)))))) H5))) h H0 H1 H2 H3))))) | (drop_drop k0 h0 c0 e H0 u0) \Rightarrow (\lambda (H1: (eq nat (S h0) h)).(\lambda (H2: (eq nat O (S d))).(\lambda (H3: (eq C (CHead c0 k0 u0) (CHead c k u))).(\lambda (H4: (eq C e x)).(eq_ind nat (S h0) (\lambda (n: nat).((eq nat O (S d)) \to ((eq C (CHead c0 k0 u0) (CHead c k u)) \to ((eq C e x) \to ((drop (r k0 h0) O c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift n (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop n (r k d) c e0))))))))) (\lambda (H5: (eq nat O (S d))).(let H6 \def (eq_ind nat O (\lambda (e0: nat).(match e0 return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H5) in (False_ind ((eq C (CHead c0 k0 u0) (CHead c k u)) \to ((eq C e x) \to ((drop (r k0 h0) O c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift (S h0) (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop (S h0) (r k d) c e0))))))) H6))) h H1 H2 H3 H4 H0))))) | (drop_skip k0 h0 d0 c0 e H0 u0) \Rightarrow (\lambda (H1: (eq nat h0 h)).(\lambda (H2: (eq nat (S d0) (S d))).(\lambda (H3: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k u))).(\lambda (H4: (eq C (CHead e k0 u0) x)).(eq_ind nat h (\lambda (n: nat).((eq nat (S d0) (S d)) \to ((eq C (CHead c0 k0 (lift n (r k0 d0) u0)) (CHead c k u)) \to ((eq C (CHead e k0 u0) x) \to ((drop n (r k0 d0) c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0))))))))) (\lambda (H5: (eq nat (S d0) (S d))).(let H6 \def (f_equal nat nat (\lambda (e0: nat).(match e0 return (\lambda (_: nat).nat) with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0) (S d) H5) in (eq_ind nat d (\lambda (n: nat).((eq C (CHead c0 k0 (lift h (r k0 n) u0)) (CHead c k u)) \to ((eq C (CHead e k0 u0) x) \to ((drop h (r k0 n) c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))))) (\lambda (H7: (eq C (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u))).(let H8 \def (f_equal C T (\lambda (e0: C).(match e0 return (\lambda (_: C).T) with [(CSort _) \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d: nat) (t: T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))]) in lref_map) (\lambda (x: nat).(plus x h)) (r k0 d) u0) | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7) in ((let H9 \def (f_equal C K (\lambda (e0: C).(match e0 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _ k _) \Rightarrow k])) (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7) in ((let H10 \def (f_equal C C (\lambda (e0: C).(match e0 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7) in (eq_ind C c (\lambda (c1: C).((eq K k0 k) \to ((eq T (lift h (r k0 d) u0) u) \to ((eq C (CHead e k0 u0) x) \to ((drop h (r k0 d) c1 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0))))))))) (\lambda (H11: (eq K k0 k)).(eq_ind K k (\lambda (k1: K).((eq T (lift h (r k1 d) u0) u) \to ((eq C (CHead e k1 u0) x) \to ((drop h (r k1 d) c e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))))) (\lambda (H12: (eq T (lift h (r k d) u0) u)).(eq_ind T (lift h (r k d) u0) (\lambda (t: T).((eq C (CHead e k u0) x) \to ((drop h (r k d) c e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0))))))) (\lambda (H13: (eq C (CHead e k u0) x)).(eq_ind C (CHead e k u0) (\lambda (c1: C).((drop h (r k d) c e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C c1 (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h (r k d) u0) (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))) (\lambda (H14: (drop h (r k d) c e)).(let H15 \def (eq_ind_r T u (\lambda (t: T).(drop h (S d) (CHead c k t) x)) H (lift h (r k d) u0) H12) in (let H16 \def (eq_ind_r C x (\lambda (c0: C).(drop h (S d) (CHead c k (lift h (r k d) u0)) c0)) H15 (CHead e k u0) H13) in (ex3_2_intro C T (\lambda (e0: C).(\lambda (v: T).(eq C (CHead e k u0) (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h (r k d) u0) (lift h (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0))) e u0 (refl_equal C (CHead e k u0)) (refl_equal T (lift h (r k d) u0)) H14)))) x H13)) u H12)) k0 (sym_eq K k0 k H11))) c0 (sym_eq C c0 c H10))) H9)) H8))) d0 (sym_eq nat d0 d H6)))) h0 (sym_eq nat h0 h H1) H2 H3 H4 H0)))))]) in (H0 (refl_equal nat h) (refl_equal nat (S d)) (refl_equal C (CHead c k u)) (refl_equal C x))))))))).

theorem drop_skip_bind:
 \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b) (lift h d u)) (CHead e (Bind b) u))))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda (H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b) d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e (Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).

theorem drop_skip_flat:
 \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h (S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
\def
 \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda (H: (drop h (S d) c e)).(\lambda (f: F).(\lambda (u: T).(eq_ind nat (r (Flat f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S d))))))))).

theorem drop_S:
 \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h: nat).((drop h O c (CHead e (Bind b) u)) \to (drop (S h) O c e))))))
\def
 \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e: C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e (Bind b) u)) \to (drop (S h) O c0 e)))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u: T).(\lambda (h: nat).(\lambda (H: (drop h O (CSort n) (CHead e (Bind b) u))).(and3_ind (eq C (CHead e (Bind b) u) (CSort n)) (eq nat h O) (eq nat O O) (drop (S h) O (CSort n) e) (\lambda (H0: (eq C (CHead e (Bind b) u) (CSort n))).(\lambda (H1: (eq nat h O)).(\lambda (_: (eq nat O O)).(eq_ind_r nat O (\lambda (n0: nat).(drop (S n0) O (CSort n) e)) (let H3 \def (eq_ind C (CHead e (Bind b) u) (\lambda (ee: C).(match ee return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H0) in (False_ind (drop (S O) O (CSort n) e) H3)) h H1)))) (drop_gen_sort n h O (CHead e (Bind b) u) H))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e: C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e (Bind b) u)) \to (drop (S h) O c0 e))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e: C).(\lambda (u: T).(\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 k t) e))) (\lambda (H0: (drop O O (CHead c0 k t) (CHead e (Bind b) u))).(let H1 \def (f_equal C C (\lambda (e0: C).(match e0 return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) H0)) in ((let H2 \def (f_equal C K (\lambda (e0: C).(match e0 return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k _) \Rightarrow k])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) H0)) in ((let H3 \def (f_equal C T (\lambda (e0: C).(match e0 return (\lambda (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t) \Rightarrow t])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) H0)) in (\lambda (H4: (eq K k (Bind b))).(\lambda (H5: (eq C c0 e)).(eq_ind C c0 (\lambda (c1: C).(drop (S O) O (CHead c0 k t) c1)) (eq_ind_r K (Bind b) (\lambda (k0: K).(drop (S O) O (CHead c0 k0 t) c0)) (drop_drop (Bind b) O c0 c0 (drop_refl c0) t) k H4) e H5)))) H2)) H1))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 k t) e)))).(\lambda (H1: (drop (S n) O (CHead c0 k t) (CHead e (Bind b) u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0: nat).(drop n0 O c0 e)) (H e u (r k n) (drop_gen_drop k c0 (CHead e (Bind b) u) t n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).

theorem drop_ctail:
 \forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c1) (CTail k u c2))))))))
\def
 \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c c2) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c) (CTail k u c2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) c2)).(\lambda (k: K).(\lambda (u: T).(and3_ind (eq C c2 (CSort n)) (eq nat h O) (eq nat d O) (drop h d (CTail k u (CSort n)) (CTail k u c2)) (\lambda (H0: (eq C c2 (CSort n))).(\lambda (H1: (eq nat h O)).(\lambda (H2: (eq nat d O)).(eq_ind_r nat O (\lambda (n0: nat).(drop n0 d (CTail k u (CSort n)) (CTail k u c2))) (eq_ind_r nat O (\lambda (n0: nat).(drop O n0 (CTail k u (CSort n)) (CTail k u c2))) (eq_ind_r C (CSort n) (\lambda (c: C).(drop O O (CTail k u (CSort n)) (CTail k u c))) (drop_refl (CTail k u (CSort n))) c2 H0) d H2) h H1)))) (drop_gen_sort n h d c2 H))))))))) (\lambda (c2: C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h: nat).((drop h d c2 c3) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c2) (CTail k u c3)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c3: C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))))))) (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop n O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)))))) (\lambda (H: (drop O O (CHead c2 k t) c3)).(\lambda (k0: K).(\lambda (u: T).(eq_ind C (CHead c2 k t) (\lambda (c: C).(drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c))) (drop_refl (CTail k0 u (CHead c2 k t))) c3 (drop_gen_refl (CHead c2 k t) c3 H))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop n O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t) c3)).(\lambda (k0: K).(\lambda (u: T).(drop_drop k n (CTail k0 u c2) (CTail k0 u c3) (IHc c3 O (r k n) (drop_gen_drop k c2 c3 t n H0) k0 u) t)))))) h)) (\lambda (n: nat).(\lambda (H: ((\forall (h: nat).((drop h n (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)))))))).(\lambda (h: nat).(\lambda (H0: (drop h (S n) (CHead c2 k t) c3)).(\lambda (k0: K).(\lambda (u: T).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k n) c2 e))) (drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H1: (eq C c3 (CHead x0 k x1))).(\lambda (H2: (eq T t (lift h (r k n) x1))).(\lambda (H3: (drop h (r k n) c2 x0)).(let H4 \def (eq_ind C c3 (\lambda (c: C).(\forall (h: nat).((drop h n (CHead c2 k t) c) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail k0 u c))))))) H (CHead x0 k x1) H1) in (eq_ind_r C (CHead x0 k x1) (\lambda (c: C).(drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c))) (let H5 \def (eq_ind T t (\lambda (t: T).(\forall (h: nat).((drop h n (CHead c2 k t) (CHead x0 k x1)) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail k0 u (CHead x0 k x1)))))))) H4 (lift h (r k n) x1) H2) in (eq_ind_r T (lift h (r k n) x1) (\lambda (t0: T).(drop h (S n) (CTail k0 u (CHead c2 k t0)) (CTail k0 u (CHead x0 k x1)))) (drop_skip k h n (CTail k0 u c2) (CTail k0 u x0) (IHc x0 (r k n) h H3 k0 u) x1) t H2)) c3 H1))))))) (drop_gen_skip_l c2 c3 t h n k H0)))))))) d))))))) c1).

theorem drop_mono:
 \forall (c: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h d c x1) \to (\forall (x2: C).((drop h d c x2) \to (eq C x1 x2)))))))
\def
 \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0 x2) \to (eq C x1 x2)))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) x1)).(\lambda (x2: C).(\lambda (H0: (drop h d (CSort n) x2)).(and3_ind (eq C x2 (CSort n)) (eq nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H1: (eq C x2 (CSort n))).(\lambda (H2: (eq nat h O)).(\lambda (H3: (eq nat d O)).(and3_ind (eq C x1 (CSort n)) (eq nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H4: (eq C x1 (CSort n))).(\lambda (H5: (eq nat h O)).(\lambda (H6: (eq nat d O)).(eq_ind_r C (CSort n) (\lambda (c0: C).(eq C x1 c0)) (let H7 \def (eq_ind nat h (\lambda (n: nat).(eq nat n O)) H2 O H5) in (let H8 \def (eq_ind nat d (\lambda (n: nat).(eq nat n O)) H3 O H6) in (eq_ind_r C (CSort n) (\lambda (c0: C).(eq C c0 (CSort n))) (refl_equal C (CSort n)) x1 H4))) x2 H1)))) (drop_gen_sort n h d x1 H))))) (drop_gen_sort n h d x2 H0))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0 x2) \to (eq C x1 x2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c0 k t) x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C x1 x2)))))) (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 k t) x1) \to (\forall (x2: C).((drop n O (CHead c0 k t) x2) \to (eq C x1 x2))))) (\lambda (H0: (drop O O (CHead c0 k t) x1)).(\lambda (x2: C).(\lambda (H1: (drop O O (CHead c0 k t) x2)).(eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C x1 c1)) (eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C c1 (CHead c0 k t))) (refl_equal C (CHead c0 k t)) x1 (drop_gen_refl (CHead c0 k t) x1 H0)) x2 (drop_gen_refl (CHead c0 k t) x2 H1))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c0 k t) x1) \to (\forall (x2: C).((drop n O (CHead c0 k t) x2) \to (eq C x1 x2)))))).(\lambda (H1: (drop (S n) O (CHead c0 k t) x1)).(\lambda (x2: C).(\lambda (H2: (drop (S n) O (CHead c0 k t) x2)).(H x1 O (r k n) (drop_gen_drop k c0 x1 t n H1) x2 (drop_gen_drop k c0 x2 t n H2))))))) h)) (\lambda (n: nat).(\lambda (H0: ((\forall (h: nat).((drop h n (CHead c0 k t) x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C x1 x2))))))).(\lambda (h: nat).(\lambda (H1: (drop h (S n) (CHead c0 k t) x1)).(\lambda (x2: C).(\lambda (H2: (drop h (S n) (CHead c0 k t) x2)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x2 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x0: C).(\lambda (x3: T).(\lambda (H3: (eq C x2 (CHead x0 k x3))).(\lambda (H4: (eq T t (lift h (r k n) x3))).(\lambda (H5: (drop h (r k n) c0 x0)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x1 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x4: C).(\lambda (x5: T).(\lambda (H6: (eq C x1 (CHead x4 k x5))).(\lambda (H7: (eq T t (lift h (r k n) x5))).(\lambda (H8: (drop h (r k n) c0 x4)).(eq_ind_r C (CHead x0 k x3) (\lambda (c1: C).(eq C x1 c1)) (let H9 \def (eq_ind C x1 (\lambda (c: C).(\forall (h: nat).((drop h n (CHead c0 k t) c) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C c x2)))))) H0 (CHead x4 k x5) H6) in (eq_ind_r C (CHead x4 k x5) (\lambda (c1: C).(eq C c1 (CHead x0 k x3))) (let H10 \def (eq_ind T t (\lambda (t: T).(\forall (h: nat).((drop h n (CHead c0 k t) (CHead x4 k x5)) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C (CHead x4 k x5) x2)))))) H9 (lift h (r k n) x5) H7) in (let H11 \def (eq_ind T t (\lambda (t: T).(eq T t (lift h (r k n) x3))) H4 (lift h (r k n) x5) H7) in (let H12 \def (eq_ind T x5 (\lambda (t: T).(\forall (h0: nat).((drop h0 n (CHead c0 k (lift h (r k n) t)) (CHead x4 k t)) \to (\forall (x2: C).((drop h0 n (CHead c0 k (lift h (r k n) t)) x2) \to (eq C (CHead x4 k t) x2)))))) H10 x3 (lift_inj x5 x3 h (r k n) H11)) in (eq_ind_r T x3 (\lambda (t0: T).(eq C (CHead x4 k t0) (CHead x0 k x3))) (sym_equal C (CHead x0 k x3) (CHead x4 k x3) (sym_equal C (CHead x4 k x3) (CHead x0 k x3) (sym_equal C (CHead x0 k x3) (CHead x4 k x3) (f_equal3 C K T C CHead x0 x4 k k x3 x3 (H x0 (r k n) h H5 x4 H8) (refl_equal K k) (refl_equal T x3))))) x5 (lift_inj x5 x3 h (r k n) H11))))) x1 H6)) x2 H3)))))) (drop_gen_skip_l c0 x1 t h n k H1))))))) (drop_gen_skip_l c0 x2 t h n k H2)))))))) d))))))) c).

theorem drop_conf_lt:
 \forall (k: K).(\forall (i: nat).(\forall (u: T).(\forall (c0: C).(\forall (c: C).((drop i O c (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus i d)) c e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop i O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))))))))))))
\def
 \lambda (k: K).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (u: T).(\forall (c0: C).(\forall (c: C).((drop n O c (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus n d)) c e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop n O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))))) (\lambda (u: T).(\lambda (c0: C).(\lambda (c: C).(\lambda (H: (drop O O c (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h (S (plus O d)) c e)).(let H1 \def (eq_ind C c (\lambda (c: C).(drop h (S (plus O d)) c e)) H0 (CHead c0 k u) (drop_gen_refl c (CHead c0 k u) H)) in (ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k (plus O d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k (plus O d)) c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C e (CHead x0 k x1))).(\lambda (H3: (eq T u (lift h (r k (plus O d)) x1))).(\lambda (H4: (drop h (r k (plus O d)) c0 x0)).(eq_ind_r C (CHead x0 k x1) (\lambda (c1: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O c1 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (eq_ind_r T (lift h (r k (plus O d)) x1) (\lambda (t: T).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T t (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T (lift h (r k (plus O d)) x1) (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x1 x0 (refl_equal T (lift h (r k d) x1)) (drop_refl (CHead x0 k x1)) H4) u H3) e H2)))))) (drop_gen_skip_l c0 e u h (plus O d) k H1))))))))))) (\lambda (i0: nat).(\lambda (H: ((\forall (u: T).(\forall (c0: C).(\forall (c: C).((drop i0 O c (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus i0 d)) c e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))))))))))))).(\lambda (u: T).(\lambda (c0: C).(\lambda (c: C).(C_ind (\lambda (c1: C).((drop (S i0) O c1 (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus (S i0) d)) c1 e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))))))))) (\lambda (n: nat).(\lambda (_: (drop (S i0) O (CSort n) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H1: (drop h (S (plus (S i0) d)) (CSort n) e)).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat (S (plus (S i0) d)) O) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (_: (eq C e (CSort n))).(\lambda (_: (eq nat h O)).(\lambda (H4: (eq nat (S (plus (S i0) d)) O)).(let H5 \def (eq_ind nat (S (plus (S i0) d)) (\lambda (ee: nat).(match ee return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) in (False_ind (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) H5))))) (drop_gen_sort n h (S (plus (S i0) d)) e H1)))))))) (\lambda (c1: C).(\lambda (H0: (((drop (S i0) O c1 (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus (S i0) d)) c1 e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))).(\lambda (k0: K).(K_ind (\lambda (k1: K).(\forall (t: T).((drop (S i0) O (CHead c1 k1 t) (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus (S i0) d)) (CHead c1 k1 t) e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c1 (Bind b) t) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0) d)) (CHead c1 (Bind b) t) e)).(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) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Bind b) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Bind b) (plus (S i0) d)) c1 x0)).(eq_ind_r C (CHead x0 (Bind b) x1) (\lambda (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (let H6 \def (H u c0 c1 (drop_gen_drop (Bind b) c1 (CHead c0 k u) t i0 H1) x0 h d H5) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O x0 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H7: (eq T u (lift h (r k d) x2))).(\lambda (H8: (drop i0 O x0 (CHead x3 k x2))).(\lambda (H9: (drop h (r k d) c0 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x2 x3 H7 (drop_drop (Bind b) i0 x0 (CHead x3 k x2) H8 x1) H9)))))) H6)) e H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Bind b) H2))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c1 (Flat f) t) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t) e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f) (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Flat f) (plus (S i0) d)) c1 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O x0 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H6: (eq T u (lift h (r k d) x2))).(\lambda (H7: (drop (S i0) O x0 (CHead x3 k x2))).(\lambda (H8: (drop h (r k d) c0 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x2 x3 H6 (drop_drop (Flat f) i0 x0 (CHead x3 k x2) H7 x1) H8)))))) (H0 (drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2))))))))) k0)))) c)))))) i)).

theorem drop_conf_ge:
 \forall (i: nat).(\forall (a: C).(\forall (c: C).((drop i O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le (plus d h) i) \to (drop (minus i h) O e a)))))))))
\def
 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (a: C).(\forall (c: C).((drop n O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le (plus d h) n) \to (drop (minus n h) O e a)))))))))) (\lambda (a: C).(\lambda (c: C).(\lambda (H: (drop O O c a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h d c e)).(\lambda (H1: (le (plus d h) O)).(let H2 \def (eq_ind C c (\lambda (c: C).(drop h d c e)) H0 a (drop_gen_refl c a H)) in (let H3 \def (match H1 return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to (drop (minus O h) O e a)))) with [le_n \Rightarrow (\lambda (H: (eq nat (plus d h) O)).(let H3 \def (f_equal nat nat (\lambda (e0: nat).e0) (plus d h) O H) 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 (H0: (eq nat d O)).(\lambda (H1: (eq nat h O)).(let H2 \def (eq_ind nat d (\lambda (n: nat).(drop h n a e)) H2 O H0) in (let H4 \def (eq_ind nat h (\lambda (n: nat).(drop n O a e)) H2 O H1) in (eq_ind C a (\lambda (c: C).(drop O O c a)) (drop_refl a) e (drop_gen_refl a e H4)))))) (plus_O d h H3)) (plus d h) H3) O H3))) | (le_S m H) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H0 \def (eq_ind nat (S m) (\lambda (e0: nat).(match e0 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (plus d h) m) \to (drop (minus O h) O e a)) H0)) H))]) 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 (n: nat).(le (plus n h) (S i0))) H2 O H5) in (let H10 \def (eq_ind nat h (\lambda (n: nat).(le (plus O n) (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 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) e)).(\lambda (H3: (le (plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Flat f) 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 (Flat f) t) e)).(\lambda (H5: (le (plus O h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 (Flat f) 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 (Flat f) t) e)).(\lambda (_: (le (plus O O) (S i0))).(eq_ind C (CHead c0 (Flat f) t) (\lambda (c1: C).(drop (minus (S i0) O) O c1 a)) (drop_drop (Flat f) i0 c0 a (drop_gen_drop (Flat f) c0 a t i0 H1) t) e (drop_gen_refl (CHead c0 (Flat f) t) e H6)))) (\lambda (h0: nat).(\lambda (_: (((drop h0 O (CHead c0 (Flat f) 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 (Flat f) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H0 (drop_gen_drop (Flat f) c0 a t i0 H1) e (S h0) O (drop_gen_drop (Flat f) c0 e t h0 H6) H7))))) h H4 H5))) (\lambda (d0: nat).(\lambda (_: (((drop h d0 (CHead c0 (Flat f) 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 (Flat f) 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 (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) d0) c0 e0))) (drop (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f) d0) x1))).(\lambda (H8: (drop h (r (Flat f) d0) c0 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (let H9 \def (eq_ind_r nat (minus (S i0) h) (\lambda (n: nat).(drop n O x0 a)) (H0 (drop_gen_drop (Flat f) c0 a t i0 H1) x0 h (S d0) H8 H5) (S (minus i0 h)) (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) in (eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Flat f) x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 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 (Flat f) H4)))))) d H2 H3))))))))) k)))) c))))) i).

theorem drop_conf_rev:
 \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop j O c1 c2)) (\lambda (c1: C).(drop i j c1 e1)))))))))
\def
 \lambda (j: nat).(nat_ind (\lambda (n: nat).(\forall (e1: C).(\forall (e2: C).((drop n O e1 e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop n O c1 c2)) (\lambda (c1: C).(drop i n c1 e1)))))))))) (\lambda (e1: C).(\lambda (e2: C).(\lambda (H: (drop O O e1 e2)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(let H1 \def (eq_ind_r C e2 (\lambda (c: C).(drop i O c2 c)) H0 e1 (drop_gen_refl e1 e2 H)) in (ex_intro2 C (\lambda (c1: C).(drop O O c1 c2)) (\lambda (c1: C).(drop i O c1 e1)) c2 (drop_refl c2) H1)))))))) (\lambda (j0: nat).(\lambda (IHj: ((\forall (e1: C).(\forall (e2: C).((drop j0 O e1 e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop j0 O c1 c2)) (\lambda (c1: C).(drop i j0 c1 e1))))))))))).(\lambda (e1: C).(C_ind (\lambda (c: C).(\forall (e2: C).((drop (S j0) O c e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 c))))))))) (\lambda (n: nat).(\lambda (e2: C).(\lambda (H: (drop (S j0) O (CSort n) e2)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(and3_ind (eq C e2 (CSort n)) (eq nat (S j0) O) (eq nat O O) (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) (\lambda (H1: (eq C e2 (CSort n))).(\lambda (H2: (eq nat (S j0) O)).(\lambda (_: (eq nat O O)).(let H4 \def (eq_ind C e2 (\lambda (c: C).(drop i O c2 c)) H0 (CSort n) H1) in (let H5 \def (eq_ind nat (S j0) (\lambda (ee: nat).(match ee return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) H5)))))) (drop_gen_sort n (S j0) O e2 H)))))))) (\lambda (e2: C).(\lambda (IHe1: ((\forall (e3: C).((drop (S j0) O e2 e3) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e3) \to (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 e2)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e3: C).(\lambda (H: (drop (S j0) O (CHead e2 k t) e3)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e3)).((match k return (\lambda (k0: K).((drop (r k0 j0) O e2 e3) \to (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 k0 t)))))) with [(Bind b) \Rightarrow (\lambda (H1: (drop (r (Bind b) j0) O e2 e3)).(let H_x \def (IHj e2 e3 H1 c2 i H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c1: C).(drop j0 O c1 c2)) (\lambda (c1: C).(drop i j0 c1 e2)) (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Bind b) t)))) (\lambda (x: C).(\lambda (H3: (drop j0 O x c2)).(\lambda (H4: (drop i j0 x e2)).(ex_intro2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Bind b) t))) (CHead x (Bind b) (lift i (r (Bind b) j0) t)) (drop_drop (Bind b) j0 x c2 H3 (lift i (r (Bind b) j0) t)) (drop_skip (Bind b) i j0 x e2 H4 t))))) H2)))) | (Flat f) \Rightarrow (\lambda (H1: (drop (r (Flat f) j0) O e2 e3)).(let H_x \def (IHe1 e3 H1 c2 i H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 e2)) (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat f) t)))) (\lambda (x: C).(\lambda (H3: (drop (S j0) O x c2)).(\lambda (H4: (drop i (S j0) x e2)).(ex_intro2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat f) t))) (CHead x (Flat f) (lift i (r (Flat f) j0) t)) (drop_drop (Flat f) j0 x c2 H3 (lift i (r (Flat f) j0) t)) (drop_skip (Flat f) i j0 x e2 H4 t))))) H2))))]) (drop_gen_drop k e2 e3 t j0 H))))))))))) e1)))) j).

theorem drop_trans_le:
 \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O c2 e2) \to (ex2 C (\lambda (e1: C).(drop i O c1 e1)) (\lambda (e1: C).(drop h (minus d i) e1 e2)))))))))))
\def
 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (d: nat).((le n d) \to (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop n O c2 e2) \to (ex2 C (\lambda (e1: C).(drop n O c1 e1)) (\lambda (e1: C).(drop h (minus d n) e1 e2)))))))))))) (\lambda (d: nat).(\lambda (_: (le O d)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (H0: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H1: (drop O O c2 e2)).(let H2 \def (eq_ind C c2 (\lambda (c: C).(drop h d c1 c)) H0 e2 (drop_gen_refl c2 e2 H1)) in (eq_ind nat d (\lambda (n: nat).(ex2 C (\lambda (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h n e1 e2)))) (ex_intro2 C (\lambda (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h d e1 e2)) c1 (drop_refl c1) H2) (minus d O) (minus_n_O d))))))))))) (\lambda (i0: nat).(\lambda (IHi: ((\forall (d: nat).((le i0 d) \to (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i0 O c2 e2) \to (ex2 C (\lambda (e1: C).(drop i0 O c1 e1)) (\lambda (e1: C).(drop h (minus d i0) e1 e2))))))))))))).(\lambda (d: nat).(nat_ind (\lambda (n: nat).((le (S i0) n) \to (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h n c1 c2) \to (\forall (e2: C).((drop (S i0) O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus n (S i0)) e1 e2))))))))))) (\lambda (H: (le (S i0) O)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (_: (drop h O c1 c2)).(\lambda (e2: C).(\lambda (_: (drop (S i0) O c2 e2)).(let H2 \def (match H return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O (S i0)) e1 e2)))))) with [le_n \Rightarrow (\lambda (H2: (eq nat (S i0) O)).(let H3 \def (eq_ind nat (S i0) (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O (S i0)) e1 e2))) H3))) | (le_S m H2) \Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S i0) m) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus O (S i0)) e1 e2)))) H4)) H2))]) in (H2 (refl_equal nat O)))))))))) (\lambda (d0: nat).(\lambda (_: (((le (S i0) d0) \to (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d0 c1 c2) \to (\forall (e2: C).((drop (S i0) O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h (minus d0 (S i0)) e1 e2)))))))))))).(\lambda (H: (le (S i0) (S d0))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (h: nat).((drop h (S d0) c c2) \to (\forall (e2: C).((drop (S i0) O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CSort n) c2)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c2 e2)).(and3_ind (eq C c2 (CSort n)) (eq nat h O) (eq nat (S d0) O) (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (H2: (eq C c2 (CSort n))).(\lambda (_: (eq nat h O)).(\lambda (_: (eq nat (S d0) O)).(let H5 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CSort n) H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O) (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (H6: (eq C e2 (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C (CSort n) (\lambda (c: C).(ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 c)))) (let H9 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7) in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 (CSort n)))) H9)) e2 H6)))) (drop_gen_sort n (S i0) O e2 H5)))))) (drop_gen_sort n h (S d0) c2 H0)))))))) (\lambda (c2: C).(\lambda (IHc: ((\forall (c3: C).(\forall (h: nat).((drop h (S d0) c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c2 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(\forall (c3: C).(\forall (h: nat).((drop h (S d0) (CHead c2 k0 t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 k0 t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (c3: C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Bind b) t) c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e (Bind b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r (Bind b) d0) c2 e))) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Bind b) t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0 (Bind b) x1))).(\lambda (H3: (eq T t (lift h (r (Bind b) d0) x1))).(\lambda (H4: (drop h (r (Bind b) d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CHead x0 (Bind b) x1) H2) in (eq_ind_r T (lift h (r (Bind b) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Bind b) t0) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)))) (ex2_ind C (\lambda (e1: C).(drop i0 O c2 e1)) (\lambda (e1: C).(drop h (minus d0 i0) e1 e2)) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x: C).(\lambda (H6: (drop i0 O c2 x)).(\lambda (H7: (drop h (minus d0 i0) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)) x (drop_drop (Bind b) i0 c2 x H6 (lift h (r (Bind b) d0) x1)) H7)))) (IHi d0 (le_S_n i0 d0 H) c2 x0 h H4 e2 (drop_gen_drop (Bind b) x0 e2 x1 i0 H5))) t H3))))))) (drop_gen_skip_l c2 c3 t h d0 (Bind b) H0))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (c3: C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Flat f) t) c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r (Flat f) d0) c2 e))) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f) t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0 (Flat f) x1))).(\lambda (H3: (eq T t (lift h (r (Flat f) d0) x1))).(\lambda (H4: (drop h (r (Flat f) d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CHead x0 (Flat f) x1) H2) in (eq_ind_r T (lift h (r (Flat f) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f) t0) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)))) (ex2_ind C (\lambda (e1: C).(drop (S i0) O c2 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f) (lift h (r (Flat f) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x: C).(\lambda (H6: (drop (S i0) O c2 x)).(\lambda (H7: (drop h (minus (S d0) (S i0)) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f) (lift h (r (Flat f) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)) x (drop_drop (Flat f) i0 c2 x H6 (lift h (r (Flat f) d0) x1)) H7)))) (IHc x0 h H4 e2 (drop_gen_drop (Flat f) x0 e2 x1 i0 H5))) t H3))))))) (drop_gen_skip_l c2 c3 t h d0 (Flat f) H0))))))))) k)))) c1))))) d)))) i).

theorem drop_trans_ge:
 \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O c2 e2) \to ((le d i) \to (drop (plus i h) O c1 e2)))))))))
\def
 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop n O c2 e2) \to ((le d n) \to (drop (plus n h) O c1 e2)))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H0: (drop O O c2 e2)).(\lambda (H1: (le d O)).(eq_ind C c2 (\lambda (c: C).(drop (plus O h) O c1 c)) (let H2 \def (match H1 return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to (drop (plus O h) O c1 c2)))) with [le_n \Rightarrow (\lambda (H0: (eq nat d O)).(eq_ind nat O (\lambda (_: nat).(drop (plus O h) O c1 c2)) (let H2 \def (eq_ind nat d (\lambda (n: nat).(le n O)) H1 O H0) in (let H3 \def (eq_ind nat d (\lambda (n: nat).(drop h n c1 c2)) H O H0) in H3)) d (sym_eq nat d O H0))) | (le_S m H0) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H1 \def (eq_ind nat (S m) (\lambda (e: nat).(match e return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le d m) \to (drop (plus O h) O c1 c2)) H1)) H0))]) in (H2 (refl_equal nat O))) e2 (drop_gen_refl c2 e2 H0)))))))))) (\lambda (i0: nat).(\lambda (IHi: ((\forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i0 O c2 e2) \to ((le d i0) \to (drop (plus i0 h) O c1 e2))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c c2) \to (\forall (e2: C).((drop (S i0) O c2 e2) \to ((le d (S i0)) \to (drop (plus (S i0) h) O c e2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) c2)).(\lambda (e2: C).(\lambda (H0: (drop (S i0) O c2 e2)).(\lambda (H1: (le d (S i0))).(and3_ind (eq C c2 (CSort n)) (eq nat h O) (eq nat d O) (drop (S (plus i0 h)) O (CSort n) e2) (\lambda (H2: (eq C c2 (CSort n))).(\lambda (H3: (eq nat h O)).(\lambda (H4: (eq nat d O)).(eq_ind_r nat O (\lambda (n0: nat).(drop (S (plus i0 n0)) O (CSort n) e2)) (let H5 \def (eq_ind nat d (\lambda (n: nat).(le n (S i0))) H1 O H4) in (let H6 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CSort n) H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O) (drop (S (plus i0 O)) O (CSort n) e2) (\lambda (H7: (eq C e2 (CSort n))).(\lambda (H8: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C (CSort n) (\lambda (c: C).(drop (S (plus i0 O)) O (CSort n) c)) (let H10 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H8) in (False_ind (drop (S (plus i0 O)) O (CSort n) (CSort n)) H10)) e2 H7)))) (drop_gen_sort n (S i0) O e2 H6)))) h H3)))) (drop_gen_sort n h d c2 H)))))))))) (\lambda (c2: C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h: nat).((drop h d c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le d (S i0)) \to (drop (S (plus i0 h)) O c2 e2)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c3: C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le n (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2))))))) (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le O (S i0)) \to (drop (S (plus i0 n)) O (CHead c2 k t) e2)))))) (\lambda (H: (drop O O (CHead c2 k t) c3)).(\lambda (e2: C).(\lambda (H0: (drop (S i0) O c3 e2)).(\lambda (_: (le O (S i0))).(let H2 \def (eq_ind_r C c3 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CHead c2 k t) (drop_gen_refl (CHead c2 k t) c3 H)) in (eq_ind nat i0 (\lambda (n: nat).(drop (S n) O (CHead c2 k t) e2)) (drop_drop k i0 c2 e2 (drop_gen_drop k c2 e2 t i0 H2) t) (plus i0 O) (plus_n_O i0))))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le O (S i0)) \to (drop (S (plus i0 n)) O (CHead c2 k t) e2))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t) c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(\lambda (H2: (le O (S i0))).(eq_ind nat (S (plus i0 n)) (\lambda (n0: nat).(drop (S n0) O (CHead c2 k t) e2)) (drop_drop k (S (plus i0 n)) c2 e2 (eq_ind_r nat (S (r k (plus i0 n))) (\lambda (n0: nat).(drop n0 O c2 e2)) (eq_ind_r nat (plus i0 (r k n)) (\lambda (n0: nat).(drop (S n0) O c2 e2)) (IHc c3 O (r k n) (drop_gen_drop k c2 c3 t n H0) e2 H1 H2) (r k (plus i0 n)) (r_plus_sym k i0 n)) (r k (S (plus i0 n))) (r_S k (plus i0 n))) t) (plus i0 (S n)) (plus_n_Sm i0 n)))))))) h)) (\lambda (d0: nat).(\lambda (IHd: ((\forall (h: nat).((drop h d0 (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le d0 (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2)))))))).(\lambda (h: nat).(\lambda (H: (drop h (S d0) (CHead c2 k t) c3)).(\lambda (e2: C).(\lambda (H0: (drop (S i0) O c3 e2)).(\lambda (H1: (le (S d0) (S i0))).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k d0) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k d0) c2 e))) (drop (S (plus i0 h)) O (CHead c2 k t) e2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0 k x1))).(\lambda (H3: (eq T t (lift h (r k d0) x1))).(\lambda (H4: (drop h (r k d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c: C).(\forall (h: nat).((drop h d0 (CHead c2 k t) c) \to (\forall (e2: C).((drop (S i0) O c e2) \to ((le d0 (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2))))))) IHd (CHead x0 k x1) H2) in (let H6 \def (eq_ind C c3 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CHead x0 k x1) H2) in (let H7 \def (eq_ind T t (\lambda (t: T).(\forall (h: nat).((drop h d0 (CHead c2 k t) (CHead x0 k x1)) \to (\forall (e2: C).((drop (S i0) O (CHead x0 k x1) e2) \to ((le d0 (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2))))))) H5 (lift h (r k d0) x1) H3) in (eq_ind_r T (lift h (r k d0) x1) (\lambda (t0: T).(drop (S (plus i0 h)) O (CHead c2 k t0) e2)) (drop_drop k (plus i0 h) c2 e2 (K_ind (\lambda (k0: K).((drop h (r k0 d0) c2 x0) \to ((drop (r k0 i0) O x0 e2) \to (drop (r k0 (plus i0 h)) O c2 e2)))) (\lambda (b: B).(\lambda (H8: (drop h (r (Bind b) d0) c2 x0)).(\lambda (H9: (drop (r (Bind b) i0) O x0 e2)).(IHi c2 x0 (r (Bind b) d0) h H8 e2 H9 (le_S_n (r (Bind b) d0) i0 H1))))) (\lambda (f: F).(\lambda (H8: (drop h (r (Flat f) d0) c2 x0)).(\lambda (H9: (drop (r (Flat f) i0) O x0 e2)).(IHc x0 (r (Flat f) d0) h H8 e2 H9 H1)))) k H4 (drop_gen_drop k x0 e2 x1 i0 H6)) (lift h (r k d0) x1)) t H3))))))))) (drop_gen_skip_l c2 c3 t h d0 k H))))))))) d))))))) c1)))) i).

inductive drop1: PList \to (C \to (C \to Prop)) \def
| drop1_nil: \forall (c: C).(drop1 PNil c c)
| drop1_cons: \forall (c1: C).(\forall (c2: C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: PList).((drop1 hds c2 c3) \to (drop1 (PCons h d hds) c1 c3)))))))).

definition ctrans:
 PList \to (nat \to (T \to T))
\def
 let rec ctrans (hds: PList) on hds: (nat \to (T \to T)) \def (\lambda (i: nat).(\lambda (t: T).(match hds with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (let j \def (trans hds0 i) in (let u \def (ctrans hds0 i t) in (match (blt j d) with [true \Rightarrow (lift h (minus d (S j)) u) | false \Rightarrow u])))]))) in ctrans.

theorem drop1_skip_bind:
 \forall (b: B).(\forall (e: C).(\forall (hds: PList).(\forall (c: C).(\forall (u: T).((drop1 hds c e) \to (drop1 (Ss hds) (CHead c (Bind b) (lift1 hds u)) (CHead e (Bind b) u)))))))
\def
 \lambda (b: B).(\lambda (e: C).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p) (CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) u)))))) (\lambda (c: C).(\lambda (u: T).(\lambda (H: (drop1 PNil c e)).(let H0 \def (match H return (\lambda (p: PList).(\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (drop1 p c0 c1)).((eq PList p PNil) \to ((eq C c0 c) \to ((eq C c1 e) \to (drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u))))))))) with [(drop1_nil c0) \Rightarrow (\lambda (_: (eq PList PNil PNil)).(\lambda (H1: (eq C c0 c)).(\lambda (H2: (eq C c0 e)).(eq_ind C c (\lambda (c1: C).((eq C c1 e) \to (drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u)))) (\lambda (H3: (eq C c e)).(eq_ind C e (\lambda (c: C).(drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u))) (drop1_nil (CHead e (Bind b) u)) c (sym_eq C c e H3))) c0 (sym_eq C c0 c H1) H2)))) | (drop1_cons c1 c2 h d H0 c3 hds H1) \Rightarrow (\lambda (H2: (eq PList (PCons h d hds) PNil)).(\lambda (H3: (eq C c1 c)).(\lambda (H4: (eq C c3 e)).((let H5 \def (eq_ind PList (PCons h d hds) (\lambda (e0: PList).(match e0 return (\lambda (_: PList).Prop) with [PNil \Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H2) in (False_ind ((eq C c1 c) \to ((eq C c3 e) \to ((drop h d c1 c2) \to ((drop1 hds c2 c3) \to (drop1 PNil (CHead c (Bind b) u) (CHead e (Bind b) u)))))) H5)) H3 H4 H0 H1))))]) in (H0 (refl_equal PList PNil) (refl_equal C c) (refl_equal C e)))))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H: ((\forall (c: C).(\forall (u: T).((drop1 p c e) \to (drop1 (Ss p) (CHead c (Bind b) (lift1 p u)) (CHead e (Bind b) u))))))).(\lambda (c: C).(\lambda (u: T).(\lambda (H0: (drop1 (PCons n n0 p) c e)).(let H1 \def (match H0 return (\lambda (p0: PList).(\lambda (c0: C).(\lambda (c1: C).(\lambda (_: (drop1 p0 c0 c1)).((eq PList p0 (PCons n n0 p)) \to ((eq C c0 c) \to ((eq C c1 e) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))))))))) with [(drop1_nil c0) \Rightarrow (\lambda (H1: (eq PList PNil (PCons n n0 p))).(\lambda (H2: (eq C c0 c)).(\lambda (H3: (eq C c0 e)).((let H4 \def (eq_ind PList PNil (\lambda (e0: PList).(match e0 return (\lambda (_: PList).Prop) with [PNil \Rightarrow True | (PCons _ _ _) \Rightarrow False])) I (PCons n n0 p) H1) in (False_ind ((eq C c0 c) \to ((eq C c0 e) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u)))) H4)) H2 H3)))) | (drop1_cons c1 c2 h d H1 c3 hds H2) \Rightarrow (\lambda (H3: (eq PList (PCons h d hds) (PCons n n0 p))).(\lambda (H4: (eq C c1 c)).(\lambda (H5: (eq C c3 e)).((let H6 \def (f_equal PList PList (\lambda (e0: PList).(match e0 return (\lambda (_: PList).PList) with [PNil \Rightarrow hds | (PCons _ _ p) \Rightarrow p])) (PCons h d hds) (PCons n n0 p) H3) in ((let H7 \def (f_equal PList nat (\lambda (e0: PList).(match e0 return (\lambda (_: PList).nat) with [PNil \Rightarrow d | (PCons _ n _) \Rightarrow n])) (PCons h d hds) (PCons n n0 p) H3) in ((let H8 \def (f_equal PList nat (\lambda (e0: PList).(match e0 return (\lambda (_: PList).nat) with [PNil \Rightarrow h | (PCons n _ _) \Rightarrow n])) (PCons h d hds) (PCons n n0 p) H3) in (eq_ind nat n (\lambda (n1: nat).((eq nat d n0) \to ((eq PList hds p) \to ((eq C c1 c) \to ((eq C c3 e) \to ((drop n1 d c1 c2) \to ((drop1 hds c2 c3) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))))))))) (\lambda (H9: (eq nat d n0)).(eq_ind nat n0 (\lambda (n1: nat).((eq PList hds p) \to ((eq C c1 c) \to ((eq C c3 e) \to ((drop n n1 c1 c2) \to ((drop1 hds c2 c3) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u)))))))) (\lambda (H10: (eq PList hds p)).(eq_ind PList p (\lambda (p0: PList).((eq C c1 c) \to ((eq C c3 e) \to ((drop n n0 c1 c2) \to ((drop1 p0 c2 c3) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))))))) (\lambda (H11: (eq C c1 c)).(eq_ind C c (\lambda (c0: C).((eq C c3 e) \to ((drop n n0 c0 c2) \to ((drop1 p c2 c3) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u)))))) (\lambda (H12: (eq C c3 e)).(eq_ind C e (\lambda (c0: C).((drop n n0 c c2) \to ((drop1 p c2 c0) \to (drop1 (PCons n (S n0) (Ss p)) (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead e (Bind b) u))))) (\lambda (H13: (drop n n0 c c2)).(\lambda (H14: (drop1 p c2 e)).(drop1_cons (CHead c (Bind b) (lift n n0 (lift1 p u))) (CHead c2 (Bind b) (lift1 p u)) n (S n0) (drop_skip_bind n n0 c c2 H13 b (lift1 p u)) (CHead e (Bind b) u) (Ss p) (H c2 u H14)))) c3 (sym_eq C c3 e H12))) c1 (sym_eq C c1 c H11))) hds (sym_eq PList hds p H10))) d (sym_eq nat d n0 H9))) h (sym_eq nat h n H8))) H7)) H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList (PCons n n0 p)) (refl_equal C c) (refl_equal C e)))))))))) hds))).

theorem drop1_cons_tail:
 \forall (c2: C).(\forall (c3: C).(\forall (h: nat).(\forall (d: nat).((drop h d c2 c3) \to (\forall (hds: PList).(\forall (c1: C).((drop1 hds c1 c2) \to (drop1 (PConsTail hds h d) c1 c3))))))))
\def
 \lambda (c2: C).(\lambda (c3: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (drop h d c2 c3)).(\lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (c1: C).((drop1 p c1 c2) \to (drop1 (PConsTail p h d) c1 c3)))) (\lambda (c1: C).(\lambda (H0: (drop1 PNil c1 c2)).(let H1 \def (match H0 return (\lambda (p: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop1 p c c0)).((eq PList p PNil) \to ((eq C c c1) \to ((eq C c0 c2) \to (drop1 (PCons h d PNil) c1 c3)))))))) with [(drop1_nil c) \Rightarrow (\lambda (_: (eq PList PNil PNil)).(\lambda (H2: (eq C c c1)).(\lambda (H3: (eq C c c2)).(eq_ind C c1 (\lambda (c0: C).((eq C c0 c2) \to (drop1 (PCons h d PNil) c1 c3))) (\lambda (H4: (eq C c1 c2)).(eq_ind C c2 (\lambda (c0: C).(drop1 (PCons h d PNil) c0 c3)) (drop1_cons c2 c3 h d H c3 PNil (drop1_nil c3)) c1 (sym_eq C c1 c2 H4))) c (sym_eq C c c1 H2) H3)))) | (drop1_cons c0 c4 h0 d0 H1 c5 hds H2) \Rightarrow (\lambda (H3: (eq PList (PCons h0 d0 hds) PNil)).(\lambda (H4: (eq C c0 c1)).(\lambda (H5: (eq C c5 c2)).((let H6 \def (eq_ind PList (PCons h0 d0 hds) (\lambda (e: PList).(match e return (\lambda (_: PList).Prop) with [PNil \Rightarrow False | (PCons _ _ _) \Rightarrow True])) I PNil H3) in (False_ind ((eq C c0 c1) \to ((eq C c5 c2) \to ((drop h0 d0 c0 c4) \to ((drop1 hds c4 c5) \to (drop1 (PCons h d PNil) c1 c3))))) H6)) H4 H5 H1 H2))))]) in (H1 (refl_equal PList PNil) (refl_equal C c1) (refl_equal C c2))))) (\lambda (n: nat).(\lambda (n0: nat).(\lambda (p: PList).(\lambda (H0: ((\forall (c1: C).((drop1 p c1 c2) \to (drop1 (PConsTail p h d) c1 c3))))).(\lambda (c1: C).(\lambda (H1: (drop1 (PCons n n0 p) c1 c2)).(let H2 \def (match H1 return (\lambda (p0: PList).(\lambda (c: C).(\lambda (c0: C).(\lambda (_: (drop1 p0 c c0)).((eq PList p0 (PCons n n0 p)) \to ((eq C c c1) \to ((eq C c0 c2) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3)))))))) with [(drop1_nil c) \Rightarrow (\lambda (H2: (eq PList PNil (PCons n n0 p))).(\lambda (H3: (eq C c c1)).(\lambda (H4: (eq C c c2)).((let H5 \def (eq_ind PList PNil (\lambda (e: PList).(match e return (\lambda (_: PList).Prop) with [PNil \Rightarrow True | (PCons _ _ _) \Rightarrow False])) I (PCons n n0 p) H2) in (False_ind ((eq C c c1) \to ((eq C c c2) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3))) H5)) H3 H4)))) | (drop1_cons c0 c4 h0 d0 H2 c5 hds H3) \Rightarrow (\lambda (H4: (eq PList (PCons h0 d0 hds) (PCons n n0 p))).(\lambda (H5: (eq C c0 c1)).(\lambda (H6: (eq C c5 c2)).((let H7 \def (f_equal PList PList (\lambda (e: PList).(match e return (\lambda (_: PList).PList) with [PNil \Rightarrow hds | (PCons _ _ p) \Rightarrow p])) (PCons h0 d0 hds) (PCons n n0 p) H4) in ((let H8 \def (f_equal PList nat (\lambda (e: PList).(match e return (\lambda (_: PList).nat) with [PNil \Rightarrow d0 | (PCons _ n _) \Rightarrow n])) (PCons h0 d0 hds) (PCons n n0 p) H4) in ((let H9 \def (f_equal PList nat (\lambda (e: PList).(match e return (\lambda (_: PList).nat) with [PNil \Rightarrow h0 | (PCons n _ _) \Rightarrow n])) (PCons h0 d0 hds) (PCons n n0 p) H4) in (eq_ind nat n (\lambda (n1: nat).((eq nat d0 n0) \to ((eq PList hds p) \to ((eq C c0 c1) \to ((eq C c5 c2) \to ((drop n1 d0 c0 c4) \to ((drop1 hds c4 c5) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3)))))))) (\lambda (H10: (eq nat d0 n0)).(eq_ind nat n0 (\lambda (n1: nat).((eq PList hds p) \to ((eq C c0 c1) \to ((eq C c5 c2) \to ((drop n n1 c0 c4) \to ((drop1 hds c4 c5) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3))))))) (\lambda (H11: (eq PList hds p)).(eq_ind PList p (\lambda (p0: PList).((eq C c0 c1) \to ((eq C c5 c2) \to ((drop n n0 c0 c4) \to ((drop1 p0 c4 c5) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3)))))) (\lambda (H12: (eq C c0 c1)).(eq_ind C c1 (\lambda (c: C).((eq C c5 c2) \to ((drop n n0 c c4) \to ((drop1 p c4 c5) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3))))) (\lambda (H13: (eq C c5 c2)).(eq_ind C c2 (\lambda (c: C).((drop n n0 c1 c4) \to ((drop1 p c4 c) \to (drop1 (PCons n n0 (PConsTail p h d)) c1 c3)))) (\lambda (H14: (drop n n0 c1 c4)).(\lambda (H15: (drop1 p c4 c2)).(drop1_cons c1 c4 n n0 H14 c3 (PConsTail p h d) (H0 c4 H15)))) c5 (sym_eq C c5 c2 H13))) c0 (sym_eq C c0 c1 H12))) hds (sym_eq PList hds p H11))) d0 (sym_eq nat d0 n0 H10))) h0 (sym_eq nat h0 n H9))) H8)) H7)) H5 H6 H2 H3))))]) in (H2 (refl_equal PList (PCons n n0 p)) (refl_equal C c1) (refl_equal C c2))))))))) hds)))))).

theorem lift1_free:
 \forall (hds: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 hds (lift (S i) O t)) (lift (S (trans hds i)) O (ctrans hds i t)))))
\def
 \lambda (hds: PList).(PList_ind (\lambda (p: PList).(\forall (i: nat).(\forall (t: T).(eq T (lift1 p (lift (S i) O t)) (lift (S (trans p i)) O (ctrans p i t)))))) (\lambda (i: nat).(\lambda (t: T).(refl_equal T (lift (S i) O t)))) (\lambda (h: nat).(\lambda (d: nat).(\lambda (hds0: PList).(\lambda (H: ((\forall (i: nat).(\forall (t: T).(eq T (lift1 hds0 (lift (S i) O t)) (lift (S (trans hds0 i)) O (ctrans hds0 i t))))))).(\lambda (i: nat).(\lambda (t: T).(eq_ind_r T (lift (S (trans hds0 i)) O (ctrans hds0 i t)) (\lambda (t0: T).(eq T (lift h d t0) (lift (S (match (blt (trans hds0 i) d) with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)])) O (match (blt (trans hds0 i) d) with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t)) | false \Rightarrow (ctrans hds0 i t)])))) (xinduction bool (blt (trans hds0 i) d) (\lambda (b: bool).(eq T (lift h d (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift (S (match b with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)])) O (match b with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t)) | false \Rightarrow (ctrans hds0 i t)])))) (\lambda (x_x: bool).(bool_ind (\lambda (b: bool).((eq bool (blt (trans hds0 i) d) b) \to (eq T (lift h d (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift (S (match b with [true \Rightarrow (trans hds0 i) | false \Rightarrow (plus (trans hds0 i) h)])) O (match b with [true \Rightarrow (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t)) | false \Rightarrow (ctrans hds0 i t)]))))) (\lambda (H0: (eq bool (blt (trans hds0 i) d) true)).(eq_ind_r nat (plus (S (trans hds0 i)) (minus d (S (trans hds0 i)))) (\lambda (n: nat).(eq T (lift h n (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t))))) (eq_ind_r T (lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t))) (\lambda (t0: T).(eq T t0 (lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t))))) (refl_equal T (lift (S (trans hds0 i)) O (lift h (minus d (S (trans hds0 i))) (ctrans hds0 i t)))) (lift h (plus (S (trans hds0 i)) (minus d (S (trans hds0 i)))) (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift_d (ctrans hds0 i t) h (S (trans hds0 i)) (minus d (S (trans hds0 i))) O (le_O_n (minus d (S (trans hds0 i)))))) d (le_plus_minus (S (trans hds0 i)) d (bge_le (S (trans hds0 i)) d (le_bge (S (trans hds0 i)) d (lt_le_S (trans hds0 i) d (blt_lt d (trans hds0 i) H0))))))) (\lambda (H0: (eq bool (blt (trans hds0 i) d) false)).(eq_ind_r T (lift (plus h (S (trans hds0 i))) O (ctrans hds0 i t)) (\lambda (t0: T).(eq T t0 (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t)))) (eq_ind nat (S (plus h (trans hds0 i))) (\lambda (n: nat).(eq T (lift n O (ctrans hds0 i t)) (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t)))) (eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O (ctrans hds0 i t)) (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t)))) (refl_equal T (lift (S (plus (trans hds0 i) h)) O (ctrans hds0 i t))) (plus h (trans hds0 i)) (plus_comm h (trans hds0 i))) (plus h (S (trans hds0 i))) (plus_n_Sm h (trans hds0 i))) (lift h d (lift (S (trans hds0 i)) O (ctrans hds0 i t))) (lift_free (ctrans hds0 i t) (S (trans hds0 i)) h O d (eq_ind nat (S (plus O (trans hds0 i))) (\lambda (n: nat).(le d n)) (eq_ind_r nat (plus (trans hds0 i) O) (\lambda (n: nat).(le d (S n))) (le_S d (plus (trans hds0 i) O) (le_plus_trans d (trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus O (trans hds0 i)) (plus_comm O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans hds0 i))) (le_O_n d)))) x_x))) (lift1 hds0 (lift (S i) O t)) (H i t)))))))) hds).

inductive clear: C \to (C \to Prop) \def
| clear_bind: \forall (b: B).(\forall (e: C).(\forall (u: T).(clear (CHead e (Bind b) u) (CHead e (Bind b) u))))
| clear_flat: \forall (e: C).(\forall (c: C).((clear e c) \to (\forall (f: F).(\forall (u: T).(clear (CHead e (Flat f) u) c))))).

inductive getl (h:nat) (c1:C) (c2:C): Prop \def
| getl_intro: \forall (e: C).((drop h O c1 e) \to ((clear e c2) \to (getl h c1 c2))).

definition cimp:
 C \to (C \to Prop)
\def
 \lambda (c1: C).(\lambda (c2: C).(\forall (b: B).(\forall (d1: C).(\forall (w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to (ex C (\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w)))))))))).

theorem clear_gen_sort:
 \forall (x: C).(\forall (n: nat).((clear (CSort n) x) \to (\forall (P: Prop).P)))
\def
 \lambda (x: C).(\lambda (n: nat).(\lambda (H: (clear (CSort n) x)).(\lambda (P: Prop).(let H0 \def (match H return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (clear c c0)).((eq C c (CSort n)) \to ((eq C c0 x) \to P))))) with [(clear_bind b e u) \Rightarrow (\lambda (H0: (eq C (CHead e (Bind b) u) (CSort n))).(\lambda (H1: (eq C (CHead e (Bind b) u) x)).((let H2 \def (eq_ind C (CHead e (Bind b) u) (\lambda (e0: C).(match e0 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H0) in (False_ind ((eq C (CHead e (Bind b) u) x) \to P) H2)) H1))) | (clear_flat e c H0 f u) \Rightarrow (\lambda (H1: (eq C (CHead e (Flat f) u) (CSort n))).(\lambda (H2: (eq C c x)).((let H3 \def (eq_ind C (CHead e (Flat f) u) (\lambda (e0: C).(match e0 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H1) in (False_ind ((eq C c x) \to ((clear e c) \to P)) H3)) H2 H0)))]) in (H0 (refl_equal C (CSort n)) (refl_equal C x)))))).

theorem clear_gen_bind:
 \forall (b: B).(\forall (e: C).(\forall (x: C).(\forall (u: T).((clear (CHead e (Bind b) u) x) \to (eq C x (CHead e (Bind b) u))))))
\def
 \lambda (b: B).(\lambda (e: C).(\lambda (x: C).(\lambda (u: T).(\lambda (H: (clear (CHead e (Bind b) u) x)).(let H0 \def (match H return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (clear c c0)).((eq C c (CHead e (Bind b) u)) \to ((eq C c0 x) \to (eq C x (CHead e (Bind b) u))))))) with [(clear_bind b0 e0 u0) \Rightarrow (\lambda (H0: (eq C (CHead e0 (Bind b0) u0) (CHead e (Bind b) u))).(\lambda (H1: (eq C (CHead e0 (Bind b0) u0) x)).((let H2 \def (f_equal C T (\lambda (e1: C).(match e1 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e0 (Bind b0) u0) (CHead e (Bind b) u) H0) in ((let H3 \def (f_equal C B (\lambda (e1: C).(match e1 return (\lambda (_: C).B) with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b0])])) (CHead e0 (Bind b0) u0) (CHead e (Bind b) u) H0) in ((let H4 \def (f_equal C C (\lambda (e1: C).(match e1 return (\lambda (_: C).C) with [(CSort _) \Rightarrow e0 | (CHead c _ _) \Rightarrow c])) (CHead e0 (Bind b0) u0) (CHead e (Bind b) u) H0) in (eq_ind C e (\lambda (c: C).((eq B b0 b) \to ((eq T u0 u) \to ((eq C (CHead c (Bind b0) u0) x) \to (eq C x (CHead e (Bind b) u)))))) (\lambda (H5: (eq B b0 b)).(eq_ind B b (\lambda (b1: B).((eq T u0 u) \to ((eq C (CHead e (Bind b1) u0) x) \to (eq C x (CHead e (Bind b) u))))) (\lambda (H6: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((eq C (CHead e (Bind b) t) x) \to (eq C x (CHead e (Bind b) u)))) (\lambda (H7: (eq C (CHead e (Bind b) u) x)).(eq_ind C (CHead e (Bind b) u) (\lambda (c: C).(eq C c (CHead e (Bind b) u))) (refl_equal C (CHead e (Bind b) u)) x H7)) u0 (sym_eq T u0 u H6))) b0 (sym_eq B b0 b H5))) e0 (sym_eq C e0 e H4))) H3)) H2)) H1))) | (clear_flat e0 c H0 f u0) \Rightarrow (\lambda (H1: (eq C (CHead e0 (Flat f) u0) (CHead e (Bind b) u))).(\lambda (H2: (eq C c x)).((let H3 \def (eq_ind C (CHead e0 (Flat f) u0) (\lambda (e1: C).(match e1 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (CHead e (Bind b) u) H1) in (False_ind ((eq C c x) \to ((clear e0 c) \to (eq C x (CHead e (Bind b) u)))) H3)) H2 H0)))]) in (H0 (refl_equal C (CHead e (Bind b) u)) (refl_equal C x))))))).

theorem clear_gen_flat:
 \forall (f: F).(\forall (e: C).(\forall (x: C).(\forall (u: T).((clear (CHead e (Flat f) u) x) \to (clear e x)))))
\def
 \lambda (f: F).(\lambda (e: C).(\lambda (x: C).(\lambda (u: T).(\lambda (H: (clear (CHead e (Flat f) u) x)).(let H0 \def (match H return (\lambda (c: C).(\lambda (c0: C).(\lambda (_: (clear c c0)).((eq C c (CHead e (Flat f) u)) \to ((eq C c0 x) \to (clear e x)))))) with [(clear_bind b e0 u0) \Rightarrow (\lambda (H0: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u))).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) x)).((let H2 \def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (e1: C).(match e1 return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H0) in (False_ind ((eq C (CHead e0 (Bind b) u0) x) \to (clear e x)) H2)) H1))) | (clear_flat e0 c H0 f0 u0) \Rightarrow (\lambda (H1: (eq C (CHead e0 (Flat f0) u0) (CHead e (Flat f) u))).(\lambda (H2: (eq C c x)).((let H3 \def (f_equal C T (\lambda (e1: C).(match e1 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead e0 (Flat f0) u0) (CHead e (Flat f) u) H1) in ((let H4 \def (f_equal C F (\lambda (e1: C).(match e1 return (\lambda (_: C).F) with [(CSort _) \Rightarrow f0 | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).F) with [(Bind _) \Rightarrow f0 | (Flat f) \Rightarrow f])])) (CHead e0 (Flat f0) u0) (CHead e (Flat f) u) H1) in ((let H5 \def (f_equal C C (\lambda (e1: C).(match e1 return (\lambda (_: C).C) with [(CSort _) \Rightarrow e0 | (CHead c _ _) \Rightarrow c])) (CHead e0 (Flat f0) u0) (CHead e (Flat f) u) H1) in (eq_ind C e (\lambda (c0: C).((eq F f0 f) \to ((eq T u0 u) \to ((eq C c x) \to ((clear c0 c) \to (clear e x)))))) (\lambda (H6: (eq F f0 f)).(eq_ind F f (\lambda (_: F).((eq T u0 u) \to ((eq C c x) \to ((clear e c) \to (clear e x))))) (\lambda (H7: (eq T u0 u)).(eq_ind T u (\lambda (_: T).((eq C c x) \to ((clear e c) \to (clear e x)))) (\lambda (H8: (eq C c x)).(eq_ind C x (\lambda (c0: C).((clear e c0) \to (clear e x))) (\lambda (H9: (clear e x)).H9) c (sym_eq C c x H8))) u0 (sym_eq T u0 u H7))) f0 (sym_eq F f0 f H6))) e0 (sym_eq C e0 e H5))) H4)) H3)) H2 H0)))]) in (H0 (refl_equal C (CHead e (Flat f) u)) (refl_equal C x))))))).

theorem clear_gen_flat_r:
 \forall (f: F).(\forall (x: C).(\forall (e: C).(\forall (u: T).((clear x (CHead e (Flat f) u)) \to (\forall (P: Prop).P)))))
\def
 \lambda (f: F).(\lambda (x: C).(\lambda (e: C).(\lambda (u: T).(\lambda (H: (clear x (CHead e (Flat f) u))).(\lambda (P: Prop).(insert_eq C (CHead e (Flat f) u) (\lambda (c: C).(clear x c)) P (\lambda (y: C).(\lambda (H0: (clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: C).((eq C c0 (CHead e (Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u))).(let H2 \def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match ee return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H1) in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda (H1: (clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to P))).(\lambda (_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) u))).(let H4 \def (eq_ind C c (\lambda (c: C).((eq C c (CHead e (Flat f) u)) \to P)) H2 (CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda (c: C).(clear e0 c)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C (CHead e (Flat f) u)))))))))))) x y H0))) H)))))).

theorem clear_gen_all:
 \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (ex_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c2 (CHead e (Bind b) u))))))))
\def
 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: (clear c1 c2)).(clear_ind (\lambda (_: C).(\lambda (c0: C).(ex_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c0 (CHead e (Bind b) u)))))))) (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(ex_3_intro B C T (\lambda (b0: B).(\lambda (e0: C).(\lambda (u0: T).(eq C (CHead e (Bind b) u) (CHead e0 (Bind b0) u0))))) b e u (refl_equal C (CHead e (Bind b) u)))))) (\lambda (e: C).(\lambda (c: C).(\lambda (H0: (clear e c)).(\lambda (H1: (ex_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c (CHead e (Bind b) u))))))).(\lambda (_: F).(\lambda (_: T).(let H2 \def H1 in (ex_3_ind B C T (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C c (CHead e0 (Bind b) u0))))) (ex_3 B C T (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C c (CHead e0 (Bind b) u0)))))) (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H3: (eq C c (CHead x1 (Bind x0) x2))).(let H4 \def (eq_ind C c (\lambda (c: C).(clear e c)) H0 (CHead x1 (Bind x0) x2) H3) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c0: C).(ex_3 B C T (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C c0 (CHead e0 (Bind b) u0))))))) (ex_3_intro B C T (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: T).(eq C (CHead x1 (Bind x0) x2) (CHead e0 (Bind b) u0))))) x0 x1 x2 (refl_equal C (CHead x1 (Bind x0) x2))) c H3)))))) H2)))))))) c1 c2 H))).

theorem drop_clear:
 \forall (c1: C).(\forall (c2: C).(\forall (i: nat).((drop (S i) O c1 c2) \to (ex2_3 B C T (\lambda (b: B).(\lambda (e: C).(\lambda (v: T).(clear c1 (CHead e (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2))))))))
\def
 \lambda (c1: C).(C_ind (\lambda (c: C).(\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 (n: nat).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H: (drop (S i) O (CSort n) c2)).(and3_ind (eq C c2 (CSort n)) (eq nat (S i) O) (eq nat O O) (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))))) (\lambda (_: (eq C c2 (CSort n))).(\lambda (H1: (eq nat (S i) O)).(\lambda (_: (eq nat O O)).(let H3 \def (eq_ind nat (S i) (\lambda (ee: nat).(match ee 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)).((match k return (\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))))))) with [(Bind b) \Rightarrow (\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)) | (Flat f) \Rightarrow (\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 (Bind b) v))))) (\lambda (_: B).(\lambda (e: C).(\lambda (_: T).(drop i O e c2)))) x0 x1 x2 (clear_flat c (CHead x1 (Bind x0) x2) H3 f t) H4)))))) H2)))]) (drop_gen_drop k c c2 t i H0))))))))) c1).

theorem drop_clear_O:
 \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (u: T).((clear c (CHead e1 (Bind b) u)) \to (\forall (e2: C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c e2))))))))
\def
 \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1: C).(\forall (u: T).((clear c0 (CHead e1 (Bind b) u)) \to (\forall (e2: C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c0 e2)))))))) (\lambda (n: nat).(\lambda (e1: C).(\lambda (u: T).(\lambda (H: (clear (CSort n) (CHead e1 (Bind b) u))).(\lambda (e2: C).(\lambda (i: nat).(\lambda (_: (drop i O e1 e2)).(clear_gen_sort (CHead e1 (Bind b) u) n H (drop (S i) O (CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1: C).(\forall (u: T).((clear c0 (CHead e1 (Bind b) u)) \to (\forall (e2: C).(\forall (i: nat).((drop i O e1 e2) \to (drop (S i) O c0 e2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (u: T).(\lambda (H0: (clear (CHead c0 k t) (CHead e1 (Bind b) u))).(\lambda (e2: C).(\lambda (i: nat).(\lambda (H1: (drop i O e1 e2)).((match k return (\lambda (k0: K).((clear (CHead c0 k0 t) (CHead e1 (Bind b) u)) \to (drop (S i) O (CHead c0 k0 t) e2))) with [(Bind b0) \Rightarrow (\lambda (H2: (clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b) u))).(let H3 \def (f_equal C C (\lambda (e: C).(match e return (\lambda (_: C).C) with [(CSort _) \Rightarrow e1 | (CHead c _ _) \Rightarrow c])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in ((let H5 \def (f_equal C T (\lambda (e: C).(match e return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead e1 (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) u) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq C e1 c0)).(let H8 \def (eq_ind C e1 (\lambda (c: C).(drop i O c e2)) H1 c0 H7) in (eq_ind B b (\lambda (b1: B).(drop (S i) O (CHead c0 (Bind b1) t) e2)) (drop_drop (Bind b) i c0 e2 H8 t) b0 H6))))) H4)) H3))) | (Flat f) \Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t) (CHead e1 (Bind b) u))).(drop_drop (Flat f) i c0 e2 (H e1 u (clear_gen_flat f c0 (CHead e1 (Bind b) u) t H2) e2 i H1) t))]) H0))))))))))) c)).

theorem drop_clear_S:
 \forall (x2: C).(\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop h (S d) x1 x2) \to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear x2 (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))))))))))
\def
 \lambda (x2: C).(C_ind (\lambda (c: C).(\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))))))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b: B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2 (Bind b) u))).(clear_gen_sort (CHead c2 (Bind b) u) n H0 (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))))))))))))) (\lambda (c: C).(\lambda (H: ((\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h (S d) x1 (CHead c k t))).(\lambda (b: B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H1: (clear (CHead c k t) (CHead c2 (Bind b) u))).(ex2_ind C (\lambda (e: C).(eq C x1 (CHead e k (lift h (r k d) t)))) (\lambda (e: C).(drop h (r k d) e c)) (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))) (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift h (r k d) t)))).(\lambda (H3: (drop h (r k d) x c)).(eq_ind_r C (CHead x k (lift h (r k d) t)) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear c0 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))) ((match k return (\lambda (k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to ((drop h (r k0 d) x c) \to (ex2 C (\lambda (c1: C).(clear (CHead x k0 (lift h (r k0 d) t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))))) with [(Bind b0) \Rightarrow (\lambda (H4: (clear (CHead c (Bind b0) t) (CHead c2 (Bind b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let H6 \def (f_equal C C (\lambda (e: C).(match e return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in ((let H7 \def (f_equal C B (\lambda (e: C).(match e return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in ((let H8 \def (f_equal C T (\lambda (e: C).(match e return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in (\lambda (H9: (eq B b b0)).(\lambda (H10: (eq C c2 c)).(eq_ind_r T t (\lambda (t0: T).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b) (lift h d t0)))) (\lambda (c1: C).(drop h d c1 c2)))) (eq_ind_r C c (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c0)))) (eq_ind_r B b0 (\lambda (b1: B).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b1) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)))) (ex_intro2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b0) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)) x (clear_bind b0 x (lift h d t)) H5) b H9) c2 H10) u H8)))) H7)) H6)))) | (Flat f) \Rightarrow (\lambda (H4: (clear (CHead c (Flat f) t) (CHead c2 (Bind b) u))).(\lambda (H5: (drop h (r (Flat f) d) x c)).(let H6 \def (H x h d H5 b c2 u (clear_gen_flat f c (CHead c2 (Bind b) u) t H4)) in (ex2_ind C (\lambda (c1: C).(clear x (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)) (ex2 C (\lambda (c1: C).(clear (CHead x (Flat f) (lift h (r (Flat f) d) t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))) (\lambda (x0: C).(\lambda (H7: (clear x (CHead x0 (Bind b) (lift h d u)))).(\lambda (H8: (drop h d x0 c2)).(ex_intro2 C (\lambda (c1: C).(clear (CHead x (Flat f) (lift h (r (Flat f) d) t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)) x0 (clear_flat x (CHead x0 (Bind b) (lift h d u)) H7 f (lift h (r (Flat f) d) t)) H8)))) H6))))]) H1 H3) x1 H2)))) (drop_gen_skip_r c x1 t h d k H0)))))))))))))) x2).

theorem clear_clear:
 \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (clear c2 c2)))
\def
 \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).((clear c c2) \to (clear c2 c2)))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (H: (clear (CSort n) c2)).(clear_gen_sort c2 n H (clear c2 c2))))) (\lambda (c: C).(\lambda (H: ((\forall (c2: C).((clear c c2) \to (clear c2 c2))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c2: C).(\lambda (H0: (clear (CHead c k t) c2)).((match k return (\lambda (k0: K).((clear (CHead c k0 t) c2) \to (clear c2 c2))) with [(Bind b) \Rightarrow (\lambda (H1: (clear (CHead c (Bind b) t) c2)).(eq_ind_r C (CHead c (Bind b) t) (\lambda (c0: C).(clear c0 c0)) (clear_bind b c t) c2 (clear_gen_bind b c c2 t H1))) | (Flat f) \Rightarrow (\lambda (H1: (clear (CHead c (Flat f) t) c2)).(H c2 (clear_gen_flat f c c2 t H1)))]) H0))))))) c1).

theorem clear_mono:
 \forall (c: C).(\forall (c1: C).((clear c c1) \to (\forall (c2: C).((clear c c2) \to (eq C c1 c2)))))
\def
 \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (c1: C).((clear c0 c1) \to (\forall (c2: C).((clear c0 c2) \to (eq C c1 c2)))))) (\lambda (n: nat).(\lambda (c1: C).(\lambda (_: (clear (CSort n) c1)).(\lambda (c2: C).(\lambda (H0: (clear (CSort n) c2)).(clear_gen_sort c2 n H0 (eq C c1 c2))))))) (\lambda (c0: C).(\lambda (H: ((\forall (c1: C).((clear c0 c1) \to (\forall (c2: C).((clear c0 c2) \to (eq C c1 c2))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c1: C).(\lambda (H0: (clear (CHead c0 k t) c1)).(\lambda (c2: C).(\lambda (H1: (clear (CHead c0 k t) c2)).((match k return (\lambda (k0: K).((clear (CHead c0 k0 t) c1) \to ((clear (CHead c0 k0 t) c2) \to (eq C c1 c2)))) with [(Bind b) \Rightarrow (\lambda (H2: (clear (CHead c0 (Bind b) t) c1)).(\lambda (H3: (clear (CHead c0 (Bind b) t) c2)).(eq_ind_r C (CHead c0 (Bind b) t) (\lambda (c3: C).(eq C c1 c3)) (eq_ind_r C (CHead c0 (Bind b) t) (\lambda (c3: C).(eq C c3 (CHead c0 (Bind b) t))) (refl_equal C (CHead c0 (Bind b) t)) c1 (clear_gen_bind b c0 c1 t H2)) c2 (clear_gen_bind b c0 c2 t H3)))) | (Flat f) \Rightarrow (\lambda (H2: (clear (CHead c0 (Flat f) t) c1)).(\lambda (H3: (clear (CHead c0 (Flat f) t) c2)).(H c1 (clear_gen_flat f c0 c1 t H2) c2 (clear_gen_flat f c0 c2 t H3))))]) H0 H1))))))))) c).

theorem clear_trans:
 \forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (c2: C).((clear c c2) \to (clear c1 c2)))))
\def
 \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c0: C).((clear c c0) \to (\forall (c2: C).((clear c0 c2) \to (clear c c2)))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H: (clear (CSort n) c)).(\lambda (c2: C).(\lambda (_: (clear c c2)).(clear_gen_sort c n H (clear (CSort n) c2))))))) (\lambda (c: C).(\lambda (H: ((\forall (c0: C).((clear c c0) \to (\forall (c2: C).((clear c0 c2) \to (clear c c2))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c0: C).(\lambda (H0: (clear (CHead c k t) c0)).(\lambda (c2: C).(\lambda (H1: (clear c0 c2)).((match k return (\lambda (k0: K).((clear (CHead c k0 t) c0) \to (clear (CHead c k0 t) c2))) with [(Bind b) \Rightarrow (\lambda (H2: (clear (CHead c (Bind b) t) c0)).(let H3 \def (eq_ind C c0 (\lambda (c: C).(clear c c2)) H1 (CHead c (Bind b) t) (clear_gen_bind b c c0 t H2)) in (eq_ind_r C (CHead c (Bind b) t) (\lambda (c3: C).(clear (CHead c (Bind b) t) c3)) (clear_bind b c t) c2 (clear_gen_bind b c c2 t H3)))) | (Flat f) \Rightarrow (\lambda (H2: (clear (CHead c (Flat f) t) c0)).(clear_flat c c2 (H c0 (clear_gen_flat f c c0 t H2) c2 H1) f t))]) H0))))))))) c1).

theorem clear_ctail:
 \forall (b: B).(\forall (c1: C).(\forall (c2: C).(\forall (u2: T).((clear c1 (CHead c2 (Bind b) u2)) \to (\forall (k: K).(\forall (u1: T).(clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))))))))
\def
 \lambda (b: B).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (u2: T).((clear c (CHead c2 (Bind b) u2)) \to (\forall (k: K).(\forall (u1: T).(clear (CTail k u1 c) (CHead (CTail k u1 c2) (Bind b) u2)))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (u2: T).(\lambda (H: (clear (CSort n) (CHead c2 (Bind b) u2))).(\lambda (k: K).(\lambda (u1: T).(match k return (\lambda (k0: K).(clear (CHead (CSort n) k0 u1) (CHead (CTail k0 u1 c2) (Bind b) u2))) with [(Bind b0) \Rightarrow (clear_gen_sort (CHead c2 (Bind b) u2) n H (clear (CHead (CSort n) (Bind b0) u1) (CHead (CTail (Bind b0) u1 c2) (Bind b) u2))) | (Flat f) \Rightarrow (clear_gen_sort (CHead c2 (Bind b) u2) n H (clear (CHead (CSort n) (Flat f) u1) (CHead (CTail (Flat f) u1 c2) (Bind b) u2)))]))))))) (\lambda (c: C).(\lambda (H: ((\forall (c2: C).(\forall (u2: T).((clear c (CHead c2 (Bind b) u2)) \to (\forall (k: K).(\forall (u1: T).(clear (CTail k u1 c) (CHead (CTail k u1 c2) (Bind b) u2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c2: C).(\lambda (u2: T).(\lambda (H0: (clear (CHead c k t) (CHead c2 (Bind b) u2))).(\lambda (k0: K).(\lambda (u1: T).((match k return (\lambda (k1: K).((clear (CHead c k1 t) (CHead c2 (Bind b) u2)) \to (clear (CHead (CTail k0 u1 c) k1 t) (CHead (CTail k0 u1 c2) (Bind b) u2)))) with [(Bind b0) \Rightarrow (\lambda (H1: (clear (CHead c (Bind b0) t) (CHead c2 (Bind b) u2))).(let H2 \def (f_equal C C (\lambda (e: C).(match e return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c _ _) \Rightarrow c])) (CHead c2 (Bind b) u2) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u2) t H1)) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k return (\lambda (_: K).B) with [(Bind b) \Rightarrow b | (Flat _) \Rightarrow b])])) (CHead c2 (Bind b) u2) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u2) t H1)) in ((let H4 \def (f_equal C T (\lambda (e: C).(match e return (\lambda (_: C).T) with [(CSort _) \Rightarrow u2 | (CHead _ _ t) \Rightarrow t])) (CHead c2 (Bind b) u2) (CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u2) t H1)) in (\lambda (H5: (eq B b b0)).(\lambda (H6: (eq C c2 c)).(eq_ind_r T t (\lambda (t0: T).(clear (CHead (CTail k0 u1 c) (Bind b0) t) (CHead (CTail k0 u1 c2) (Bind b) t0))) (eq_ind_r C c (\lambda (c0: C).(clear (CHead (CTail k0 u1 c) (Bind b0) t) (CHead (CTail k0 u1 c0) (Bind b) t))) (eq_ind B b (\lambda (b1: B).(clear (CHead (CTail k0 u1 c) (Bind b1) t) (CHead (CTail k0 u1 c) (Bind b) t))) (clear_bind b (CTail k0 u1 c) t) b0 H5) c2 H6) u2 H4)))) H3)) H2))) | (Flat f) \Rightarrow (\lambda (H1: (clear (CHead c (Flat f) t) (CHead c2 (Bind b) u2))).(clear_flat (CTail k0 u1 c) (CHead (CTail k0 u1 c2) (Bind b) u2) (H c2 u2 (clear_gen_flat f c (CHead c2 (Bind b) u2) t H1) k0 u1) f t))]) H0)))))))))) c1)).