]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1/drop/fwd.ma
news for matita 0.99.3
[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / drop / fwd.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "basic_1/drop/defs.ma".
18
19 include "basic_1/lift/fwd.ma".
20
21 include "basic_1/r/props.ma".
22
23 include "basic_1/C/fwd.ma".
24
25 implied rec lemma drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f: 
26 (\forall (c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall 
27 (c: C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to 
28 (\forall (u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k: 
29 K).(\forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop 
30 h (r k d) c e) \to ((P h (r k d) c e) \to (\forall (u: T).(P h (S d) (CHead c 
31 k (lift h (r k d) u)) (CHead e k u))))))))))) (n: nat) (n0: nat) (c: C) (c0: 
32 C) (d: drop n n0 c c0) on d: P n n0 c c0 \def match d with [(drop_refl c1) 
33 \Rightarrow (f c1) | (drop_drop k h c1 e d0 u) \Rightarrow (f0 k h c1 e d0 
34 ((drop_ind P f f0 f1) (r k h) O c1 e d0) u) | (drop_skip k h d0 c1 e d1 u) 
35 \Rightarrow (f1 k h d0 c1 e d1 ((drop_ind P f f0 f1) h (r k d0) c1 e d1) u)].
36
37 lemma drop_gen_sort:
38  \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(\forall (x: C).((drop 
39 h d (CSort n) x) \to (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O))))))
40 \def
41  \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (x: 
42 C).(\lambda (H: (drop h d (CSort n) x)).(insert_eq C (CSort n) (\lambda (c: 
43 C).(drop h d c x)) (\lambda (c: C).(and3 (eq C x c) (eq nat h O) (eq nat d 
44 O))) (\lambda (y: C).(\lambda (H0: (drop h d y x)).(drop_ind (\lambda (n0: 
45 nat).(\lambda (n1: nat).(\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n)) 
46 \to (and3 (eq C c0 c) (eq nat n0 O) (eq nat n1 O))))))) (\lambda (c: 
47 C).(\lambda (H1: (eq C c (CSort n))).(let H2 \def (f_equal C C (\lambda (e: 
48 C).e) c (CSort n) H1) in (eq_ind_r C (CSort n) (\lambda (c0: C).(and3 (eq C 
49 c0 c0) (eq nat O O) (eq nat O O))) (and3_intro (eq C (CSort n) (CSort n)) (eq 
50 nat O O) (eq nat O O) (refl_equal C (CSort n)) (refl_equal nat O) (refl_equal 
51 nat O)) c H2)))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (c: C).(\lambda 
52 (e: C).(\lambda (_: (drop (r k h0) O c e)).(\lambda (_: (((eq C c (CSort n)) 
53 \to (and3 (eq C e c) (eq nat (r k h0) O) (eq nat O O))))).(\lambda (u: 
54 T).(\lambda (H3: (eq C (CHead c k u) (CSort n))).(let H4 \def (eq_ind C 
55 (CHead c k u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | 
56 (CHead _ _ _) \Rightarrow True])) I (CSort n) H3) in (False_ind (and3 (eq C e 
57 (CHead c k u)) (eq nat (S h0) O) (eq nat O O)) H4)))))))))) (\lambda (k: 
58 K).(\lambda (h0: nat).(\lambda (d0: nat).(\lambda (c: C).(\lambda (e: 
59 C).(\lambda (_: (drop h0 (r k d0) c e)).(\lambda (_: (((eq C c (CSort n)) \to 
60 (and3 (eq C e c) (eq nat h0 O) (eq nat (r k d0) O))))).(\lambda (u: 
61 T).(\lambda (H3: (eq C (CHead c k (lift h0 (r k d0) u)) (CSort n))).(let H4 
62 \def (eq_ind C (CHead c k (lift h0 (r k d0) u)) (\lambda (ee: C).(match ee 
63 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I 
64 (CSort n) H3) in (False_ind (and3 (eq C (CHead e k u) (CHead c k (lift h0 (r 
65 k d0) u))) (eq nat h0 O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) 
66 H))))).
67
68 lemma drop_gen_refl:
69  \forall (x: C).(\forall (e: C).((drop O O x e) \to (eq C x e)))
70 \def
71  \lambda (x: C).(\lambda (e: C).(\lambda (H: (drop O O x e)).(insert_eq nat O 
72 (\lambda (n: nat).(drop n O x e)) (\lambda (_: nat).(eq C x e)) (\lambda (y: 
73 nat).(\lambda (H0: (drop y O x e)).(insert_eq nat O (\lambda (n: nat).(drop y 
74 n x e)) (\lambda (n: nat).((eq nat y n) \to (eq C x e))) (\lambda (y0: 
75 nat).(\lambda (H1: (drop y y0 x e)).(drop_ind (\lambda (n: nat).(\lambda (n0: 
76 nat).(\lambda (c: C).(\lambda (c0: C).((eq nat n0 O) \to ((eq nat n n0) \to 
77 (eq C c c0))))))) (\lambda (c: C).(\lambda (_: (eq nat O O)).(\lambda (_: (eq 
78 nat O O)).(refl_equal C c)))) (\lambda (k: K).(\lambda (h: nat).(\lambda (c: 
79 C).(\lambda (e0: C).(\lambda (_: (drop (r k h) O c e0)).(\lambda (_: (((eq 
80 nat O O) \to ((eq nat (r k h) O) \to (eq C c e0))))).(\lambda (u: T).(\lambda 
81 (_: (eq nat O O)).(\lambda (H5: (eq nat (S h) O)).(let H6 \def (eq_ind nat (S 
82 h) (\lambda (ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow 
83 True])) I O H5) in (False_ind (eq C (CHead c k u) e0) H6))))))))))) (\lambda 
84 (k: K).(\lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e0: 
85 C).(\lambda (H2: (drop h (r k d) c e0)).(\lambda (H3: (((eq nat (r k d) O) 
86 \to ((eq nat h (r k d)) \to (eq C c e0))))).(\lambda (u: T).(\lambda (H4: (eq 
87 nat (S d) O)).(\lambda (H5: (eq nat h (S d))).(let H6 \def (f_equal nat nat 
88 (\lambda (e1: nat).e1) h (S d) H5) in (let H7 \def (eq_ind nat h (\lambda (n: 
89 nat).((eq nat (r k d) O) \to ((eq nat n (r k d)) \to (eq C c e0)))) H3 (S d) 
90 H6) in (let H8 \def (eq_ind nat h (\lambda (n: nat).(drop n (r k d) c e0)) H2 
91 (S d) H6) in (eq_ind_r nat (S d) (\lambda (n: nat).(eq C (CHead c k (lift n 
92 (r k d) u)) (CHead e0 k u))) (let H9 \def (eq_ind nat (S d) (\lambda (ee: 
93 nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4) 
94 in (False_ind (eq C (CHead c k (lift (S d) (r k d) u)) (CHead e0 k u)) H9)) h 
95 H6)))))))))))))) y y0 x e H1))) H0))) H))).
96
97 lemma drop_gen_drop:
98  \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: 
99 nat).((drop (S h) O (CHead c k u) x) \to (drop (r k h) O c x))))))
100 \def
101  \lambda (k: K).(\lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: 
102 nat).(\lambda (H: (drop (S h) O (CHead c k u) x)).(insert_eq C (CHead c k u) 
103 (\lambda (c0: C).(drop (S h) O c0 x)) (\lambda (_: C).(drop (r k h) O c x)) 
104 (\lambda (y: C).(\lambda (H0: (drop (S h) O y x)).(insert_eq nat O (\lambda 
105 (n: nat).(drop (S h) n y x)) (\lambda (n: nat).((eq C y (CHead c k u)) \to 
106 (drop (r k h) n c x))) (\lambda (y0: nat).(\lambda (H1: (drop (S h) y0 y 
107 x)).(insert_eq nat (S h) (\lambda (n: nat).(drop n y0 y x)) (\lambda (_: 
108 nat).((eq nat y0 O) \to ((eq C y (CHead c k u)) \to (drop (r k h) y0 c x)))) 
109 (\lambda (y1: nat).(\lambda (H2: (drop y1 y0 y x)).(drop_ind (\lambda (n: 
110 nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq nat n (S h)) 
111 \to ((eq nat n0 O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) n0 c 
112 c1)))))))) (\lambda (c0: C).(\lambda (H3: (eq nat O (S h))).(\lambda (_: (eq 
113 nat O O)).(\lambda (H5: (eq C c0 (CHead c k u))).(eq_ind_r C (CHead c k u) 
114 (\lambda (c1: C).(drop (r k h) O c c1)) (let H6 \def (eq_ind nat O (\lambda 
115 (ee: nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I 
116 (S h) H3) in (False_ind (drop (r k h) O c (CHead c k u)) H6)) c0 H5))))) 
117 (\lambda (k0: K).(\lambda (h0: nat).(\lambda (c0: C).(\lambda (e: C).(\lambda 
118 (H3: (drop (r k0 h0) O c0 e)).(\lambda (H4: (((eq nat (r k0 h0) (S h)) \to 
119 ((eq nat O O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) O c 
120 e)))))).(\lambda (u0: T).(\lambda (H5: (eq nat (S h0) (S h))).(\lambda (_: 
121 (eq nat O O)).(\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c k u))).(let H8 
122 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow c0 | 
123 (CHead c1 _ _) \Rightarrow c1])) (CHead c0 k0 u0) (CHead c k u) H7) in ((let 
124 H9 \def (f_equal C K (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow 
125 k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 u0) (CHead c k u) H7) in 
126 ((let H10 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _) 
127 \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 u0) (CHead c k 
128 u) H7) in (\lambda (H11: (eq K k0 k)).(\lambda (H12: (eq C c0 c)).(let H13 
129 \def (eq_ind C c0 (\lambda (c1: C).((eq nat (r k0 h0) (S h)) \to ((eq nat O 
130 O) \to ((eq C c1 (CHead c k u)) \to (drop (r k h) O c e))))) H4 c H12) in 
131 (let H14 \def (eq_ind C c0 (\lambda (c1: C).(drop (r k0 h0) O c1 e)) H3 c 
132 H12) in (let H15 \def (eq_ind K k0 (\lambda (k1: K).((eq nat (r k1 h0) (S h)) 
133 \to ((eq nat O O) \to ((eq C c (CHead c k u)) \to (drop (r k h) O c e))))) 
134 H13 k H11) in (let H16 \def (eq_ind K k0 (\lambda (k1: K).(drop (r k1 h0) O c 
135 e)) H14 k H11) in (let H17 \def (f_equal nat nat (\lambda (e0: nat).(match e0 
136 with [O \Rightarrow h0 | (S n) \Rightarrow n])) (S h0) (S h) H5) in (let H18 
137 \def (eq_ind nat h0 (\lambda (n: nat).((eq nat (r k n) (S h)) \to ((eq nat O 
138 O) \to ((eq C c (CHead c k u)) \to (drop (r k h) O c e))))) H15 h H17) in 
139 (let H19 \def (eq_ind nat h0 (\lambda (n: nat).(drop (r k n) O c e)) H16 h 
140 H17) in H19)))))))))) H9)) H8)))))))))))) (\lambda (k0: K).(\lambda (h0: 
141 nat).(\lambda (d: nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (H3: (drop 
142 h0 (r k0 d) c0 e)).(\lambda (H4: (((eq nat h0 (S h)) \to ((eq nat (r k0 d) O) 
143 \to ((eq C c0 (CHead c k u)) \to (drop (r k h) (r k0 d) c e)))))).(\lambda 
144 (u0: T).(\lambda (H5: (eq nat h0 (S h))).(\lambda (H6: (eq nat (S d) 
145 O)).(\lambda (H7: (eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k 
146 u))).(let H8 \def (eq_ind nat h0 (\lambda (n: nat).(eq C (CHead c0 k0 (lift n 
147 (r k0 d) u0)) (CHead c k u))) H7 (S h) H5) in (let H9 \def (eq_ind nat h0 
148 (\lambda (n: nat).((eq nat n (S h)) \to ((eq nat (r k0 d) O) \to ((eq C c0 
149 (CHead c k u)) \to (drop (r k h) (r k0 d) c e))))) H4 (S h) H5) in (let H10 
150 \def (eq_ind nat h0 (\lambda (n: nat).(drop n (r k0 d) c0 e)) H3 (S h) H5) in 
151 (let H11 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) 
152 \Rightarrow c0 | (CHead c1 _ _) \Rightarrow c1])) (CHead c0 k0 (lift (S h) (r 
153 k0 d) u0)) (CHead c k u) H8) in ((let H12 \def (f_equal C K (\lambda (e0: 
154 C).(match e0 with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow 
155 k1])) (CHead c0 k0 (lift (S h) (r k0 d) u0)) (CHead c k u) H8) in ((let H13 
156 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow 
157 (lref_map (\lambda (x0: nat).(plus x0 (S h))) (r k0 d) u0) | (CHead _ _ t) 
158 \Rightarrow t])) (CHead c0 k0 (lift (S h) (r k0 d) u0)) (CHead c k u) H8) in 
159 (\lambda (H14: (eq K k0 k)).(\lambda (H15: (eq C c0 c)).(let H16 \def (eq_ind 
160 C c0 (\lambda (c1: C).((eq nat (S h) (S h)) \to ((eq nat (r k0 d) O) \to ((eq 
161 C c1 (CHead c k u)) \to (drop (r k h) (r k0 d) c e))))) H9 c H15) in (let H17 
162 \def (eq_ind C c0 (\lambda (c1: C).(drop (S h) (r k0 d) c1 e)) H10 c H15) in 
163 (let H18 \def (eq_ind K k0 (\lambda (k1: K).(eq T (lift (S h) (r k1 d) u0) 
164 u)) H13 k H14) in (let H19 \def (eq_ind K k0 (\lambda (k1: K).((eq nat (S h) 
165 (S h)) \to ((eq nat (r k1 d) O) \to ((eq C c (CHead c k u)) \to (drop (r k h) 
166 (r k1 d) c e))))) H16 k H14) in (let H20 \def (eq_ind K k0 (\lambda (k1: 
167 K).(drop (S h) (r k1 d) c e)) H17 k H14) in (eq_ind_r K k (\lambda (k1: 
168 K).(drop (r k h) (S d) c (CHead e k1 u0))) (let H21 \def (eq_ind_r T u 
169 (\lambda (t: T).((eq nat (S h) (S h)) \to ((eq nat (r k d) O) \to ((eq C c 
170 (CHead c k t)) \to (drop (r k h) (r k d) c e))))) H19 (lift (S h) (r k d) u0) 
171 H18) in (let H22 \def (eq_ind nat (S d) (\lambda (ee: nat).(match ee with [O 
172 \Rightarrow False | (S _) \Rightarrow True])) I O H6) in (False_ind (drop (r 
173 k h) (S d) c (CHead e k u0)) H22))) k0 H14))))))))) H12)) H11)))))))))))))))) 
174 y1 y0 y x H2))) H1))) H0))) H)))))).
175
176 lemma drop_gen_skip_r:
177  \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall 
178 (d: nat).(\forall (k: K).((drop h (S d) x (CHead c k u)) \to (ex2 C (\lambda 
179 (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e: C).(drop h (r k 
180 d) e c)))))))))
181 \def
182  \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda 
183 (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) x (CHead c k 
184 u))).(insert_eq C (CHead c k u) (\lambda (c0: C).(drop h (S d) x c0)) 
185 (\lambda (_: C).(ex2 C (\lambda (e: C).(eq C x (CHead e k (lift h (r k d) 
186 u)))) (\lambda (e: C).(drop h (r k d) e c)))) (\lambda (y: C).(\lambda (H0: 
187 (drop h (S d) x y)).(insert_eq nat (S d) (\lambda (n: nat).(drop h n x y)) 
188 (\lambda (_: nat).((eq C y (CHead c k u)) \to (ex2 C (\lambda (e: C).(eq C x 
189 (CHead e k (lift h (r k d) u)))) (\lambda (e: C).(drop h (r k d) e c))))) 
190 (\lambda (y0: nat).(\lambda (H1: (drop h y0 x y)).(drop_ind (\lambda (n: 
191 nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq nat n0 (S d)) 
192 \to ((eq C c1 (CHead c k u)) \to (ex2 C (\lambda (e: C).(eq C c0 (CHead e k 
193 (lift n (r k d) u)))) (\lambda (e: C).(drop n (r k d) e c))))))))) (\lambda 
194 (c0: C).(\lambda (H2: (eq nat O (S d))).(\lambda (H3: (eq C c0 (CHead c k 
195 u))).(eq_ind_r C (CHead c k u) (\lambda (c1: C).(ex2 C (\lambda (e: C).(eq C 
196 c1 (CHead e k (lift O (r k d) u)))) (\lambda (e: C).(drop O (r k d) e c)))) 
197 (let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee with [O \Rightarrow 
198 True | (S _) \Rightarrow False])) I (S d) H2) in (False_ind (ex2 C (\lambda 
199 (e: C).(eq C (CHead c k u) (CHead e k (lift O (r k d) u)))) (\lambda (e: 
200 C).(drop O (r k d) e c))) H4)) c0 H3)))) (\lambda (k0: K).(\lambda (h0: 
201 nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (H2: (drop (r k0 h0) O c0 
202 e)).(\lambda (H3: (((eq nat O (S d)) \to ((eq C e (CHead c k u)) \to (ex2 C 
203 (\lambda (e0: C).(eq C c0 (CHead e0 k (lift (r k0 h0) (r k d) u)))) (\lambda 
204 (e0: C).(drop (r k0 h0) (r k d) e0 c))))))).(\lambda (u0: T).(\lambda (H4: 
205 (eq nat O (S d))).(\lambda (H5: (eq C e (CHead c k u))).(let H6 \def (eq_ind 
206 C e (\lambda (c1: C).((eq nat O (S d)) \to ((eq C c1 (CHead c k u)) \to (ex2 
207 C (\lambda (e0: C).(eq C c0 (CHead e0 k (lift (r k0 h0) (r k d) u)))) 
208 (\lambda (e0: C).(drop (r k0 h0) (r k d) e0 c)))))) H3 (CHead c k u) H5) in 
209 (let H7 \def (eq_ind C e (\lambda (c1: C).(drop (r k0 h0) O c0 c1)) H2 (CHead 
210 c k u) H5) in (let H8 \def (eq_ind nat O (\lambda (ee: nat).(match ee with [O 
211 \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4) in (False_ind (ex2 
212 C (\lambda (e0: C).(eq C (CHead c0 k0 u0) (CHead e0 k (lift (S h0) (r k d) 
213 u)))) (\lambda (e0: C).(drop (S h0) (r k d) e0 c))) H8))))))))))))) (\lambda 
214 (k0: K).(\lambda (h0: nat).(\lambda (d0: nat).(\lambda (c0: C).(\lambda (e: 
215 C).(\lambda (H2: (drop h0 (r k0 d0) c0 e)).(\lambda (H3: (((eq nat (r k0 d0) 
216 (S d)) \to ((eq C e (CHead c k u)) \to (ex2 C (\lambda (e0: C).(eq C c0 
217 (CHead e0 k (lift h0 (r k d) u)))) (\lambda (e0: C).(drop h0 (r k d) e0 
218 c))))))).(\lambda (u0: T).(\lambda (H4: (eq nat (S d0) (S d))).(\lambda (H5: 
219 (eq C (CHead e k0 u0) (CHead c k u))).(let H6 \def (f_equal C C (\lambda (e0: 
220 C).(match e0 with [(CSort _) \Rightarrow e | (CHead c1 _ _) \Rightarrow c1])) 
221 (CHead e k0 u0) (CHead c k u) H5) in ((let H7 \def (f_equal C K (\lambda (e0: 
222 C).(match e0 with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow 
223 k1])) (CHead e k0 u0) (CHead c k u) H5) in ((let H8 \def (f_equal C T 
224 (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow u0 | (CHead _ _ t) 
225 \Rightarrow t])) (CHead e k0 u0) (CHead c k u) H5) in (\lambda (H9: (eq K k0 
226 k)).(\lambda (H10: (eq C e c)).(eq_ind_r T u (\lambda (t: T).(ex2 C (\lambda 
227 (e0: C).(eq C (CHead c0 k0 (lift h0 (r k0 d0) t)) (CHead e0 k (lift h0 (r k 
228 d) u)))) (\lambda (e0: C).(drop h0 (r k d) e0 c)))) (let H11 \def (eq_ind C e 
229 (\lambda (c1: C).((eq nat (r k0 d0) (S d)) \to ((eq C c1 (CHead c k u)) \to 
230 (ex2 C (\lambda (e0: C).(eq C c0 (CHead e0 k (lift h0 (r k d) u)))) (\lambda 
231 (e0: C).(drop h0 (r k d) e0 c)))))) H3 c H10) in (let H12 \def (eq_ind C e 
232 (\lambda (c1: C).(drop h0 (r k0 d0) c0 c1)) H2 c H10) in (let H13 \def 
233 (eq_ind K k0 (\lambda (k1: K).((eq nat (r k1 d0) (S d)) \to ((eq C c (CHead c 
234 k u)) \to (ex2 C (\lambda (e0: C).(eq C c0 (CHead e0 k (lift h0 (r k d) u)))) 
235 (\lambda (e0: C).(drop h0 (r k d) e0 c)))))) H11 k H9) in (let H14 \def 
236 (eq_ind K k0 (\lambda (k1: K).(drop h0 (r k1 d0) c0 c)) H12 k H9) in 
237 (eq_ind_r K k (\lambda (k1: K).(ex2 C (\lambda (e0: C).(eq C (CHead c0 k1 
238 (lift h0 (r k1 d0) u)) (CHead e0 k (lift h0 (r k d) u)))) (\lambda (e0: 
239 C).(drop h0 (r k d) e0 c)))) (let H15 \def (f_equal nat nat (\lambda (e0: 
240 nat).(match e0 with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0) (S d) 
241 H4) in (let H16 \def (eq_ind nat d0 (\lambda (n: nat).((eq nat (r k n) (S d)) 
242 \to ((eq C c (CHead c k u)) \to (ex2 C (\lambda (e0: C).(eq C c0 (CHead e0 k 
243 (lift h0 (r k d) u)))) (\lambda (e0: C).(drop h0 (r k d) e0 c)))))) H13 d 
244 H15) in (let H17 \def (eq_ind nat d0 (\lambda (n: nat).(drop h0 (r k n) c0 
245 c)) H14 d H15) in (eq_ind_r nat d (\lambda (n: nat).(ex2 C (\lambda (e0: 
246 C).(eq C (CHead c0 k (lift h0 (r k n) u)) (CHead e0 k (lift h0 (r k d) u)))) 
247 (\lambda (e0: C).(drop h0 (r k d) e0 c)))) (ex_intro2 C (\lambda (e0: C).(eq 
248 C (CHead c0 k (lift h0 (r k d) u)) (CHead e0 k (lift h0 (r k d) u)))) 
249 (\lambda (e0: C).(drop h0 (r k d) e0 c)) c0 (refl_equal C (CHead c0 k (lift 
250 h0 (r k d) u))) H17) d0 H15)))) k0 H9))))) u0 H8)))) H7)) H6)))))))))))) h y0 
251 x y H1))) H0))) H))))))).
252
253 lemma drop_gen_skip_l:
254  \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall 
255 (d: nat).(\forall (k: K).((drop h (S d) (CHead c k u) x) \to (ex3_2 C T 
256 (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_: 
257 C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_: 
258 T).(drop h (r k d) c e))))))))))
259 \def
260  \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda 
261 (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) (CHead c k u) 
262 x)).(insert_eq C (CHead c k u) (\lambda (c0: C).(drop h (S d) c0 x)) (\lambda 
263 (_: C).(ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) 
264 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: 
265 C).(\lambda (_: T).(drop h (r k d) c e))))) (\lambda (y: C).(\lambda (H0: 
266 (drop h (S d) y x)).(insert_eq nat (S d) (\lambda (n: nat).(drop h n y x)) 
267 (\lambda (_: nat).((eq C y (CHead c k u)) \to (ex3_2 C T (\lambda (e: 
268 C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_: C).(\lambda (v: 
269 T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k 
270 d) c e)))))) (\lambda (y0: nat).(\lambda (H1: (drop h y0 y x)).(drop_ind 
271 (\lambda (n: nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq 
272 nat n0 (S d)) \to ((eq C c0 (CHead c k u)) \to (ex3_2 C T (\lambda (e: 
273 C).(\lambda (v: T).(eq C c1 (CHead e k v)))) (\lambda (_: C).(\lambda (v: 
274 T).(eq T u (lift n (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop n (r k 
275 d) c e)))))))))) (\lambda (c0: C).(\lambda (H2: (eq nat O (S d))).(\lambda 
276 (H3: (eq C c0 (CHead c k u))).(eq_ind_r C (CHead c k u) (\lambda (c1: 
277 C).(ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C c1 (CHead e k v)))) 
278 (\lambda (_: C).(\lambda (v: T).(eq T u (lift O (r k d) v)))) (\lambda (e: 
279 C).(\lambda (_: T).(drop O (r k d) c e))))) (let H4 \def (eq_ind nat O 
280 (\lambda (ee: nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow 
281 False])) I (S d) H2) in (False_ind (ex3_2 C T (\lambda (e: C).(\lambda (v: 
282 T).(eq C (CHead c k u) (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T 
283 u (lift O (r k d) v)))) (\lambda (e: C).(\lambda (_: T).(drop O (r k d) c 
284 e)))) H4)) c0 H3)))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda (c0: 
285 C).(\lambda (e: C).(\lambda (H2: (drop (r k0 h0) O c0 e)).(\lambda (H3: (((eq 
286 nat O (S d)) \to ((eq C c0 (CHead c k u)) \to (ex3_2 C T (\lambda (e0: 
287 C).(\lambda (v: T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: 
288 T).(eq T u (lift (r k0 h0) (r k d) v)))) (\lambda (e0: C).(\lambda (_: 
289 T).(drop (r k0 h0) (r k d) c e0)))))))).(\lambda (u0: T).(\lambda (H4: (eq 
290 nat O (S d))).(\lambda (H5: (eq C (CHead c0 k0 u0) (CHead c k u))).(let H6 
291 \def (f_equal C C (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow c0 | 
292 (CHead c1 _ _) \Rightarrow c1])) (CHead c0 k0 u0) (CHead c k u) H5) in ((let 
293 H7 \def (f_equal C K (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow 
294 k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 u0) (CHead c k u) H5) in 
295 ((let H8 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _) 
296 \Rightarrow u0 | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 u0) (CHead c k 
297 u) H5) in (\lambda (H9: (eq K k0 k)).(\lambda (H10: (eq C c0 c)).(let H11 
298 \def (eq_ind C c0 (\lambda (c1: C).((eq nat O (S d)) \to ((eq C c1 (CHead c k 
299 u)) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v)))) 
300 (\lambda (_: C).(\lambda (v: T).(eq T u (lift (r k0 h0) (r k d) v)))) 
301 (\lambda (e0: C).(\lambda (_: T).(drop (r k0 h0) (r k d) c e0))))))) H3 c 
302 H10) in (let H12 \def (eq_ind C c0 (\lambda (c1: C).(drop (r k0 h0) O c1 e)) 
303 H2 c H10) in (let H13 \def (eq_ind K k0 (\lambda (k1: K).((eq nat O (S d)) 
304 \to ((eq C c (CHead c k u)) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: 
305 T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift (r 
306 k1 h0) (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop (r k1 h0) (r k d) 
307 c e0))))))) H11 k H9) in (let H14 \def (eq_ind K k0 (\lambda (k1: K).(drop (r 
308 k1 h0) O c e)) H12 k H9) in (let H15 \def (eq_ind nat O (\lambda (ee: 
309 nat).(match ee with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) 
310 H4) in (False_ind (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead 
311 e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift (S h0) (r k d) v)))) 
312 (\lambda (e0: C).(\lambda (_: T).(drop (S h0) (r k d) c e0)))) H15))))))))) 
313 H7)) H6))))))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda (d0: 
314 nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (H2: (drop h0 (r k0 d0) c0 
315 e)).(\lambda (H3: (((eq nat (r k0 d0) (S d)) \to ((eq C c0 (CHead c k u)) \to 
316 (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v)))) 
317 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h0 (r k d) v)))) (\lambda (e0: 
318 C).(\lambda (_: T).(drop h0 (r k d) c e0)))))))).(\lambda (u0: T).(\lambda 
319 (H4: (eq nat (S d0) (S d))).(\lambda (H5: (eq C (CHead c0 k0 (lift h0 (r k0 
320 d0) u0)) (CHead c k u))).(let H6 \def (f_equal C C (\lambda (e0: C).(match e0 
321 with [(CSort _) \Rightarrow c0 | (CHead c1 _ _) \Rightarrow c1])) (CHead c0 
322 k0 (lift h0 (r k0 d0) u0)) (CHead c k u) H5) in ((let H7 \def (f_equal C K 
323 (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow k0 | (CHead _ k1 _) 
324 \Rightarrow k1])) (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k u) H5) in 
325 ((let H8 \def (f_equal C T (\lambda (e0: C).(match e0 with [(CSort _) 
326 \Rightarrow (lref_map (\lambda (x0: nat).(plus x0 h0)) (r k0 d0) u0) | (CHead 
327 _ _ t) \Rightarrow t])) (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k u) 
328 H5) in (\lambda (H9: (eq K k0 k)).(\lambda (H10: (eq C c0 c)).(let H11 \def 
329 (eq_ind C c0 (\lambda (c1: C).((eq nat (r k0 d0) (S d)) \to ((eq C c1 (CHead 
330 c k u)) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k 
331 v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h0 (r k d) v)))) (\lambda 
332 (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0))))))) H3 c H10) in (let H12 
333 \def (eq_ind C c0 (\lambda (c1: C).(drop h0 (r k0 d0) c1 e)) H2 c H10) in 
334 (let H13 \def (eq_ind K k0 (\lambda (k1: K).(eq T (lift h0 (r k1 d0) u0) u)) 
335 H8 k H9) in (let H14 \def (eq_ind K k0 (\lambda (k1: K).((eq nat (r k1 d0) (S 
336 d)) \to ((eq C c (CHead c k u)) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: 
337 T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h0 
338 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0))))))) 
339 H11 k H9) in (let H15 \def (eq_ind K k0 (\lambda (k1: K).(drop h0 (r k1 d0) c 
340 e)) H12 k H9) in (eq_ind_r K k (\lambda (k1: K).(ex3_2 C T (\lambda (e0: 
341 C).(\lambda (v: T).(eq C (CHead e k1 u0) (CHead e0 k v)))) (\lambda (_: 
342 C).(\lambda (v: T).(eq T u (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda 
343 (_: T).(drop h0 (r k d) c e0))))) (let H16 \def (eq_ind_r T u (\lambda (t: 
344 T).((eq nat (r k d0) (S d)) \to ((eq C c (CHead c k t)) \to (ex3_2 C T 
345 (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v)))) (\lambda (_: 
346 C).(\lambda (v: T).(eq T t (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda 
347 (_: T).(drop h0 (r k d) c e0))))))) H14 (lift h0 (r k d0) u0) H13) in (eq_ind 
348 T (lift h0 (r k d0) u0) (\lambda (t: T).(ex3_2 C T (\lambda (e0: C).(\lambda 
349 (v: T).(eq C (CHead e k u0) (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: 
350 T).(eq T t (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 
351 (r k d) c e0))))) (let H17 \def (f_equal nat nat (\lambda (e0: nat).(match e0 
352 with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0) (S d) H4) in (let H18 
353 \def (eq_ind nat d0 (\lambda (n: nat).((eq nat (r k n) (S d)) \to ((eq C c 
354 (CHead c k (lift h0 (r k n) u0))) \to (ex3_2 C T (\lambda (e0: C).(\lambda 
355 (v: T).(eq C e (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift 
356 h0 (r k n) u0) (lift h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop 
357 h0 (r k d) c e0))))))) H16 d H17) in (let H19 \def (eq_ind nat d0 (\lambda 
358 (n: nat).(drop h0 (r k n) c e)) H15 d H17) in (eq_ind_r nat d (\lambda (n: 
359 nat).(ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C (CHead e k u0) (CHead 
360 e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h0 (r k n) u0) (lift 
361 h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0))))) 
362 (ex3_2_intro C T (\lambda (e0: C).(\lambda (v: T).(eq C (CHead e k u0) (CHead 
363 e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T (lift h0 (r k d) u0) (lift 
364 h0 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h0 (r k d) c e0))) e 
365 u0 (refl_equal C (CHead e k u0)) (refl_equal T (lift h0 (r k d) u0)) H19) d0 
366 H17)))) u H13)) k0 H9))))))))) H7)) H6)))))))))))) h y0 y x H1))) H0))) 
367 H))))))).
368
369 lemma drop_S:
370  \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h: 
371 nat).((drop h O c (CHead e (Bind b) u)) \to (drop (S h) O c e))))))
372 \def
373  \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e: 
374 C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e (Bind b) u)) \to 
375 (drop (S h) O c0 e)))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u: 
376 T).(\lambda (h: nat).(\lambda (H: (drop h O (CSort n) (CHead e (Bind b) 
377 u))).(and3_ind (eq C (CHead e (Bind b) u) (CSort n)) (eq nat h O) (eq nat O 
378 O) (drop (S h) O (CSort n) e) (\lambda (H0: (eq C (CHead e (Bind b) u) (CSort 
379 n))).(\lambda (H1: (eq nat h O)).(\lambda (_: (eq nat O O)).(eq_ind_r nat O 
380 (\lambda (n0: nat).(drop (S n0) O (CSort n) e)) (let H3 \def (eq_ind C (CHead 
381 e (Bind b) u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | 
382 (CHead _ _ _) \Rightarrow True])) I (CSort n) H0) in (False_ind (drop (S O) O 
383 (CSort n) e) H3)) h H1)))) (drop_gen_sort n h O (CHead e (Bind b) u) H))))))) 
384 (\lambda (c0: C).(\lambda (H: ((\forall (e: C).(\forall (u: T).(\forall (h: 
385 nat).((drop h O c0 (CHead e (Bind b) u)) \to (drop (S h) O c0 
386 e))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e: C).(\lambda (u: 
387 T).(\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 k t) 
388 (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 k t) e))) (\lambda (H0: 
389 (drop O O (CHead c0 k t) (CHead e (Bind b) u))).(let H1 \def (f_equal C C 
390 (\lambda (e0: C).(match e0 with [(CSort _) \Rightarrow c0 | (CHead c1 _ _) 
391 \Rightarrow c1])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead 
392 c0 k t) (CHead e (Bind b) u) H0)) in ((let H2 \def (f_equal C K (\lambda (e0: 
393 C).(match e0 with [(CSort _) \Rightarrow k | (CHead _ k0 _) \Rightarrow k0])) 
394 (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead e 
395 (Bind b) u) H0)) in ((let H3 \def (f_equal C T (\lambda (e0: C).(match e0 
396 with [(CSort _) \Rightarrow t | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 k 
397 t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) 
398 H0)) in (\lambda (H4: (eq K k (Bind b))).(\lambda (H5: (eq C c0 e)).(eq_ind C 
399 c0 (\lambda (c1: C).(drop (S O) O (CHead c0 k t) c1)) (eq_ind_r K (Bind b) 
400 (\lambda (k0: K).(drop (S O) O (CHead c0 k0 t) c0)) (drop_drop (Bind b) O c0 
401 c0 (drop_refl c0) t) k H4) e H5)))) H2)) H1))) (\lambda (n: nat).(\lambda (_: 
402 (((drop n O (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 
403 k t) e)))).(\lambda (H1: (drop (S n) O (CHead c0 k t) (CHead e (Bind b) 
404 u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0: 
405 nat).(drop n0 O c0 e)) (H e u (r k n) (drop_gen_drop k c0 (CHead e (Bind b) 
406 u) t n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
407
408 theorem drop_mono:
409  \forall (c: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h 
410 d c x1) \to (\forall (x2: C).((drop h d c x2) \to (eq C x1 x2)))))))
411 \def
412  \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (x1: C).(\forall (d: 
413 nat).(\forall (h: nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0 
414 x2) \to (eq C x1 x2)))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (d: 
415 nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) x1)).(\lambda (x2: 
416 C).(\lambda (H0: (drop h d (CSort n) x2)).(and3_ind (eq C x2 (CSort n)) (eq 
417 nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H1: (eq C x2 (CSort 
418 n))).(\lambda (H2: (eq nat h O)).(\lambda (H3: (eq nat d O)).(and3_ind (eq C 
419 x1 (CSort n)) (eq nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H4: (eq C x1 
420 (CSort n))).(\lambda (H5: (eq nat h O)).(\lambda (H6: (eq nat d O)).(eq_ind_r 
421 C (CSort n) (\lambda (c0: C).(eq C x1 c0)) (let H7 \def (eq_ind nat h 
422 (\lambda (n0: nat).(eq nat n0 O)) H2 O H5) in (let H8 \def (eq_ind nat d 
423 (\lambda (n0: nat).(eq nat n0 O)) H3 O H6) in (eq_ind_r C (CSort n) (\lambda 
424 (c0: C).(eq C c0 (CSort n))) (refl_equal C (CSort n)) x1 H4))) x2 H1)))) 
425 (drop_gen_sort n h d x1 H))))) (drop_gen_sort n h d x2 H0))))))))) (\lambda 
426 (c0: C).(\lambda (H: ((\forall (x1: C).(\forall (d: nat).(\forall (h: 
427 nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0 x2) \to (eq C x1 
428 x2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (d: 
429 nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c0 k t) 
430 x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C x1 x2)))))) 
431 (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 k t) x1) 
432 \to (\forall (x2: C).((drop n O (CHead c0 k t) x2) \to (eq C x1 x2))))) 
433 (\lambda (H0: (drop O O (CHead c0 k t) x1)).(\lambda (x2: C).(\lambda (H1: 
434 (drop O O (CHead c0 k t) x2)).(eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C 
435 x1 c1)) (eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C c1 (CHead c0 k t))) 
436 (refl_equal C (CHead c0 k t)) x1 (drop_gen_refl (CHead c0 k t) x1 H0)) x2 
437 (drop_gen_refl (CHead c0 k t) x2 H1))))) (\lambda (n: nat).(\lambda (_: 
438 (((drop n O (CHead c0 k t) x1) \to (\forall (x2: C).((drop n O (CHead c0 k t) 
439 x2) \to (eq C x1 x2)))))).(\lambda (H1: (drop (S n) O (CHead c0 k t) 
440 x1)).(\lambda (x2: C).(\lambda (H2: (drop (S n) O (CHead c0 k t) x2)).(H x1 O 
441 (r k n) (drop_gen_drop k c0 x1 t n H1) x2 (drop_gen_drop k c0 x2 t n 
442 H2))))))) h)) (\lambda (n: nat).(\lambda (H0: ((\forall (h: nat).((drop h n 
443 (CHead c0 k t) x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq 
444 C x1 x2))))))).(\lambda (h: nat).(\lambda (H1: (drop h (S n) (CHead c0 k t) 
445 x1)).(\lambda (x2: C).(\lambda (H2: (drop h (S n) (CHead c0 k t) 
446 x2)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x2 (CHead e k v)))) 
447 (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e: 
448 C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x0: 
449 C).(\lambda (x3: T).(\lambda (H3: (eq C x2 (CHead x0 k x3))).(\lambda (H4: 
450 (eq T t (lift h (r k n) x3))).(\lambda (H5: (drop h (r k n) c0 
451 x0)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x1 (CHead e k v)))) 
452 (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e: 
453 C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x4: 
454 C).(\lambda (x5: T).(\lambda (H6: (eq C x1 (CHead x4 k x5))).(\lambda (H7: 
455 (eq T t (lift h (r k n) x5))).(\lambda (H8: (drop h (r k n) c0 x4)).(eq_ind_r 
456 C (CHead x0 k x3) (\lambda (c1: C).(eq C x1 c1)) (let H9 \def (eq_ind C x1 
457 (\lambda (c1: C).(\forall (h0: nat).((drop h0 n (CHead c0 k t) c1) \to 
458 (\forall (x6: C).((drop h0 n (CHead c0 k t) x6) \to (eq C c1 x6)))))) H0 
459 (CHead x4 k x5) H6) in (eq_ind_r C (CHead x4 k x5) (\lambda (c1: C).(eq C c1 
460 (CHead x0 k x3))) (let H10 \def (eq_ind T t (\lambda (t0: T).(\forall (h0: 
461 nat).((drop h0 n (CHead c0 k t0) (CHead x4 k x5)) \to (\forall (x6: C).((drop 
462 h0 n (CHead c0 k t0) x6) \to (eq C (CHead x4 k x5) x6)))))) H9 (lift h (r k 
463 n) x5) H7) in (let H11 \def (eq_ind T t (\lambda (t0: T).(eq T t0 (lift h (r 
464 k n) x3))) H4 (lift h (r k n) x5) H7) in (let H12 \def (eq_ind T x5 (\lambda 
465 (t0: T).(\forall (h0: nat).((drop h0 n (CHead c0 k (lift h (r k n) t0)) 
466 (CHead x4 k t0)) \to (\forall (x6: C).((drop h0 n (CHead c0 k (lift h (r k n) 
467 t0)) x6) \to (eq C (CHead x4 k t0) x6)))))) H10 x3 (lift_inj x5 x3 h (r k n) 
468 H11)) in (eq_ind_r T x3 (\lambda (t0: T).(eq C (CHead x4 k t0) (CHead x0 k 
469 x3))) (sym_eq C (CHead x0 k x3) (CHead x4 k x3) (sym_eq C (CHead x4 k x3) 
470 (CHead x0 k x3) (sym_eq C (CHead x0 k x3) (CHead x4 k x3) (f_equal3 C K T C 
471 CHead x0 x4 k k x3 x3 (H x0 (r k n) h H5 x4 H8) (refl_equal K k) (refl_equal 
472 T x3))))) x5 (lift_inj x5 x3 h (r k n) H11))))) x1 H6)) x2 H3)))))) 
473 (drop_gen_skip_l c0 x1 t h n k H1))))))) (drop_gen_skip_l c0 x2 t h n k 
474 H2)))))))) d))))))) c).
475