+C).(\lambda (v: T).(eq T t (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda
+(_: T).(drop h0 (r k d) c e0))))))) H14 (lift h0 (r k d0) u0) H13) in (eq_ind
+T (lift h0 (r k d0) u0) (\lambda (t: T).(ex3_2 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 t (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0
+(r k d) c e0))))) (let H17 \def (f_equal nat nat (\lambda (e0: nat).(match e0
+with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0) (S d) H4) in (let H18
+\def (eq_ind nat d0 (\lambda (n: nat).((eq nat (r k n) (S d)) \to ((eq C c
+(CHead c k (lift h0 (r k n) u0))) \to (ex3_2 C T (\lambda (e0: C).(\lambda
+(v: T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift
+h0 (r k n) u0) (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop
+h0 (r k d) c e0))))))) H16 d H17) in (let H19 \def (eq_ind nat d0 (\lambda
+(n: nat).(drop h0 (r k n) c e)) H15 d H17) in (eq_ind_r nat d (\lambda (n:
+nat).(ex3_2 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 h0 (r k n) u0) (lift
+h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0)))))
+(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 h0 (r k d) u0) (lift
+h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0))) e
+u0 (refl_equal C (CHead e k u0)) (refl_equal T (lift h0 (r k d) u0)) H19) d0
+H17)))) u H13)) k0 H9))))))))) H7)) H6)))))))))))) h y0 y x H1))) H0)))
+H))))))).
+
+lemma 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 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 with [(CSort _) \Rightarrow c0 | (CHead c1 _ _)
+\Rightarrow c1])) (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 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0]))
+(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
+with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (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_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 (n0: nat).(eq nat n0 O)) H2 O H5) in (let H8 \def (eq_ind nat d
+(\lambda (n0: nat).(eq nat n0 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 (c1: C).(\forall (h0: nat).((drop h0 n (CHead c0 k t) c1) \to
+(\forall (x6: C).((drop h0 n (CHead c0 k t) x6) \to (eq C c1 x6)))))) 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 (t0: T).(\forall (h0:
+nat).((drop h0 n (CHead c0 k t0) (CHead x4 k x5)) \to (\forall (x6: C).((drop
+h0 n (CHead c0 k t0) x6) \to (eq C (CHead x4 k x5) x6)))))) H9 (lift h (r k
+n) x5) H7) in (let H11 \def (eq_ind T t (\lambda (t0: T).(eq T t0 (lift h (r
+k n) x3))) H4 (lift h (r k n) x5) H7) in (let H12 \def (eq_ind T x5 (\lambda
+(t0: T).(\forall (h0: nat).((drop h0 n (CHead c0 k (lift h (r k n) t0))
+(CHead x4 k t0)) \to (\forall (x6: C).((drop h0 n (CHead c0 k (lift h (r k n)
+t0)) x6) \to (eq C (CHead x4 k t0) x6)))))) 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_eq C (CHead x0 k x3) (CHead x4 k x3) (sym_eq C (CHead x4 k x3)
+(CHead x0 k x3) (sym_eq 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).