1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props".
19 include "drop/defs.ma".
21 include "lift/props.ma".
23 theorem drop_skip_bind:
24 \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
25 d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b)
26 (lift h d u)) (CHead e (Bind b) u))))))))
28 \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda
29 (H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b)
30 d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e
31 (Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
33 theorem drop_skip_flat:
34 \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h
35 (S d) c e) \to (\forall (f: F).(\forall (u: T).(drop h (S d) (CHead c (Flat
36 f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
38 \lambda (h: nat).(\lambda (d: nat).(\lambda (c: C).(\lambda (e: C).(\lambda
39 (H: (drop h (S d) c e)).(\lambda (f: F).(\lambda (u: T).(eq_ind nat (r (Flat
40 f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead
41 e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S
45 \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h:
46 nat).((drop h O c (CHead e (Bind b) u)) \to (drop (S h) O c e))))))
48 \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e:
49 C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e (Bind b) u)) \to
50 (drop (S h) O c0 e)))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u:
51 T).(\lambda (h: nat).(\lambda (H: (drop h O (CSort n) (CHead e (Bind b)
52 u))).(and3_ind (eq C (CHead e (Bind b) u) (CSort n)) (eq nat h O) (eq nat O
53 O) (drop (S h) O (CSort n) e) (\lambda (H0: (eq C (CHead e (Bind b) u) (CSort
54 n))).(\lambda (H1: (eq nat h O)).(\lambda (_: (eq nat O O)).(eq_ind_r nat O
55 (\lambda (n0: nat).(drop (S n0) O (CSort n) e)) (let H3 \def (eq_ind C (CHead
56 e (Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop)
57 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
58 (CSort n) H0) in (False_ind (drop (S O) O (CSort n) e) H3)) h H1))))
59 (drop_gen_sort n h O (CHead e (Bind b) u) H))))))) (\lambda (c0: C).(\lambda
60 (H: ((\forall (e: C).(\forall (u: T).(\forall (h: nat).((drop h O c0 (CHead e
61 (Bind b) u)) \to (drop (S h) O c0 e))))))).(\lambda (k: K).(\lambda (t:
62 T).(\lambda (e: C).(\lambda (u: T).(\lambda (h: nat).(nat_ind (\lambda (n:
63 nat).((drop n O (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S n) O (CHead
64 c0 k t) e))) (\lambda (H0: (drop O O (CHead c0 k t) (CHead e (Bind b)
65 u))).(let H1 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
66 (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow
67 c])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0 k t) (CHead
68 e (Bind b) u) H0)) in ((let H2 \def (f_equal C K (\lambda (e0: C).(match e0
69 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k _)
70 \Rightarrow k])) (CHead c0 k t) (CHead e (Bind b) u) (drop_gen_refl (CHead c0
71 k t) (CHead e (Bind b) u) H0)) in ((let H3 \def (f_equal C T (\lambda (e0:
72 C).(match e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t |
73 (CHead _ _ t) \Rightarrow t])) (CHead c0 k t) (CHead e (Bind b) u)
74 (drop_gen_refl (CHead c0 k t) (CHead e (Bind b) u) H0)) in (\lambda (H4: (eq
75 K k (Bind b))).(\lambda (H5: (eq C c0 e)).(eq_ind C c0 (\lambda (c1: C).(drop
76 (S O) O (CHead c0 k t) c1)) (eq_ind_r K (Bind b) (\lambda (k0: K).(drop (S O)
77 O (CHead c0 k0 t) c0)) (drop_drop (Bind b) O c0 c0 (drop_refl c0) t) k H4) e
78 H5)))) H2)) H1))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c0 k t)
79 (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 k t) e)))).(\lambda (H1:
80 (drop (S n) O (CHead c0 k t) (CHead e (Bind b) u))).(drop_drop k (S n) c0 e
81 (eq_ind_r nat (S (r k n)) (\lambda (n0: nat).(drop n0 O c0 e)) (H e u (r k n)
82 (drop_gen_drop k c0 (CHead e (Bind b) u) t n H1)) (r k (S n)) (r_S k n))
86 \forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop
87 h d c1 c2) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k u c1)
90 \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (d:
91 nat).(\forall (h: nat).((drop h d c c2) \to (\forall (k: K).(\forall (u:
92 T).(drop h d (CTail k u c) (CTail k u c2))))))))) (\lambda (n: nat).(\lambda
93 (c2: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n)
94 c2)).(\lambda (k: K).(\lambda (u: T).(and3_ind (eq C c2 (CSort n)) (eq nat h
95 O) (eq nat d O) (drop h d (CTail k u (CSort n)) (CTail k u c2)) (\lambda (H0:
96 (eq C c2 (CSort n))).(\lambda (H1: (eq nat h O)).(\lambda (H2: (eq nat d
97 O)).(eq_ind_r nat O (\lambda (n0: nat).(drop n0 d (CTail k u (CSort n))
98 (CTail k u c2))) (eq_ind_r nat O (\lambda (n0: nat).(drop O n0 (CTail k u
99 (CSort n)) (CTail k u c2))) (eq_ind_r C (CSort n) (\lambda (c: C).(drop O O
100 (CTail k u (CSort n)) (CTail k u c))) (drop_refl (CTail k u (CSort n))) c2
101 H0) d H2) h H1)))) (drop_gen_sort n h d c2 H))))))))) (\lambda (c2:
102 C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h:
103 nat).((drop h d c2 c3) \to (\forall (k: K).(\forall (u: T).(drop h d (CTail k
104 u c2) (CTail k u c3)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c3:
105 C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n
106 (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u
107 (CHead c2 k t)) (CTail k0 u c3))))))) (\lambda (h: nat).(nat_ind (\lambda (n:
108 nat).((drop n O (CHead c2 k t) c3) \to (\forall (k0: K).(\forall (u: T).(drop
109 n O (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)))))) (\lambda (H: (drop O O
110 (CHead c2 k t) c3)).(\lambda (k0: K).(\lambda (u: T).(eq_ind C (CHead c2 k t)
111 (\lambda (c: C).(drop O O (CTail k0 u (CHead c2 k t)) (CTail k0 u c)))
112 (drop_refl (CTail k0 u (CHead c2 k t))) c3 (drop_gen_refl (CHead c2 k t) c3
113 H))))) (\lambda (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to
114 (\forall (k0: K).(\forall (u: T).(drop n O (CTail k0 u (CHead c2 k t)) (CTail
115 k0 u c3))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t) c3)).(\lambda (k0:
116 K).(\lambda (u: T).(drop_drop k n (CTail k0 u c2) (CTail k0 u c3) (IHc c3 O
117 (r k n) (drop_gen_drop k c2 c3 t n H0) k0 u) t)))))) h)) (\lambda (n:
118 nat).(\lambda (H: ((\forall (h: nat).((drop h n (CHead c2 k t) c3) \to
119 (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t)) (CTail
120 k0 u c3)))))))).(\lambda (h: nat).(\lambda (H0: (drop h (S n) (CHead c2 k t)
121 c3)).(\lambda (k0: K).(\lambda (u: T).(ex3_2_ind C T (\lambda (e: C).(\lambda
122 (v: T).(eq C c3 (CHead e k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
123 (lift h (r k n) v)))) (\lambda (e: C).(\lambda (_: T).(drop h (r k n) c2 e)))
124 (drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c3)) (\lambda (x0:
125 C).(\lambda (x1: T).(\lambda (H1: (eq C c3 (CHead x0 k x1))).(\lambda (H2:
126 (eq T t (lift h (r k n) x1))).(\lambda (H3: (drop h (r k n) c2 x0)).(let H4
127 \def (eq_ind C c3 (\lambda (c: C).(\forall (h: nat).((drop h n (CHead c2 k t)
128 c) \to (\forall (k0: K).(\forall (u: T).(drop h n (CTail k0 u (CHead c2 k t))
129 (CTail k0 u c))))))) H (CHead x0 k x1) H1) in (eq_ind_r C (CHead x0 k x1)
130 (\lambda (c: C).(drop h (S n) (CTail k0 u (CHead c2 k t)) (CTail k0 u c)))
131 (let H5 \def (eq_ind T t (\lambda (t: T).(\forall (h: nat).((drop h n (CHead
132 c2 k t) (CHead x0 k x1)) \to (\forall (k0: K).(\forall (u: T).(drop h n
133 (CTail k0 u (CHead c2 k t)) (CTail k0 u (CHead x0 k x1)))))))) H4 (lift h (r
134 k n) x1) H2) in (eq_ind_r T (lift h (r k n) x1) (\lambda (t0: T).(drop h (S
135 n) (CTail k0 u (CHead c2 k t0)) (CTail k0 u (CHead x0 k x1)))) (drop_skip k h
136 n (CTail k0 u c2) (CTail k0 u x0) (IHc x0 (r k n) h H3 k0 u) x1) t H2)) c3
137 H1))))))) (drop_gen_skip_l c2 c3 t h n k H0)))))))) d))))))) c1).
140 \forall (c: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h
141 d c x1) \to (\forall (x2: C).((drop h d c x2) \to (eq C x1 x2)))))))
143 \lambda (c: C).(C_ind (\lambda (c0: C).(\forall (x1: C).(\forall (d:
144 nat).(\forall (h: nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0
145 x2) \to (eq C x1 x2)))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (d:
146 nat).(\lambda (h: nat).(\lambda (H: (drop h d (CSort n) x1)).(\lambda (x2:
147 C).(\lambda (H0: (drop h d (CSort n) x2)).(and3_ind (eq C x2 (CSort n)) (eq
148 nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H1: (eq C x2 (CSort
149 n))).(\lambda (H2: (eq nat h O)).(\lambda (H3: (eq nat d O)).(and3_ind (eq C
150 x1 (CSort n)) (eq nat h O) (eq nat d O) (eq C x1 x2) (\lambda (H4: (eq C x1
151 (CSort n))).(\lambda (H5: (eq nat h O)).(\lambda (H6: (eq nat d O)).(eq_ind_r
152 C (CSort n) (\lambda (c0: C).(eq C x1 c0)) (let H7 \def (eq_ind nat h
153 (\lambda (n: nat).(eq nat n O)) H2 O H5) in (let H8 \def (eq_ind nat d
154 (\lambda (n: nat).(eq nat n O)) H3 O H6) in (eq_ind_r C (CSort n) (\lambda
155 (c0: C).(eq C c0 (CSort n))) (refl_equal C (CSort n)) x1 H4))) x2 H1))))
156 (drop_gen_sort n h d x1 H))))) (drop_gen_sort n h d x2 H0))))))))) (\lambda
157 (c0: C).(\lambda (H: ((\forall (x1: C).(\forall (d: nat).(\forall (h:
158 nat).((drop h d c0 x1) \to (\forall (x2: C).((drop h d c0 x2) \to (eq C x1
159 x2))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (d:
160 nat).(nat_ind (\lambda (n: nat).(\forall (h: nat).((drop h n (CHead c0 k t)
161 x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C x1 x2))))))
162 (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c0 k t) x1)
163 \to (\forall (x2: C).((drop n O (CHead c0 k t) x2) \to (eq C x1 x2)))))
164 (\lambda (H0: (drop O O (CHead c0 k t) x1)).(\lambda (x2: C).(\lambda (H1:
165 (drop O O (CHead c0 k t) x2)).(eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C
166 x1 c1)) (eq_ind C (CHead c0 k t) (\lambda (c1: C).(eq C c1 (CHead c0 k t)))
167 (refl_equal C (CHead c0 k t)) x1 (drop_gen_refl (CHead c0 k t) x1 H0)) x2
168 (drop_gen_refl (CHead c0 k t) x2 H1))))) (\lambda (n: nat).(\lambda (_:
169 (((drop n O (CHead c0 k t) x1) \to (\forall (x2: C).((drop n O (CHead c0 k t)
170 x2) \to (eq C x1 x2)))))).(\lambda (H1: (drop (S n) O (CHead c0 k t)
171 x1)).(\lambda (x2: C).(\lambda (H2: (drop (S n) O (CHead c0 k t) x2)).(H x1 O
172 (r k n) (drop_gen_drop k c0 x1 t n H1) x2 (drop_gen_drop k c0 x2 t n
173 H2))))))) h)) (\lambda (n: nat).(\lambda (H0: ((\forall (h: nat).((drop h n
174 (CHead c0 k t) x1) \to (\forall (x2: C).((drop h n (CHead c0 k t) x2) \to (eq
175 C x1 x2))))))).(\lambda (h: nat).(\lambda (H1: (drop h (S n) (CHead c0 k t)
176 x1)).(\lambda (x2: C).(\lambda (H2: (drop h (S n) (CHead c0 k t)
177 x2)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x2 (CHead e k v))))
178 (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e:
179 C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x0:
180 C).(\lambda (x3: T).(\lambda (H3: (eq C x2 (CHead x0 k x3))).(\lambda (H4:
181 (eq T t (lift h (r k n) x3))).(\lambda (H5: (drop h (r k n) c0
182 x0)).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C x1 (CHead e k v))))
183 (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k n) v)))) (\lambda (e:
184 C).(\lambda (_: T).(drop h (r k n) c0 e))) (eq C x1 x2) (\lambda (x4:
185 C).(\lambda (x5: T).(\lambda (H6: (eq C x1 (CHead x4 k x5))).(\lambda (H7:
186 (eq T t (lift h (r k n) x5))).(\lambda (H8: (drop h (r k n) c0 x4)).(eq_ind_r
187 C (CHead x0 k x3) (\lambda (c1: C).(eq C x1 c1)) (let H9 \def (eq_ind C x1
188 (\lambda (c: C).(\forall (h: nat).((drop h n (CHead c0 k t) c) \to (\forall
189 (x2: C).((drop h n (CHead c0 k t) x2) \to (eq C c x2)))))) H0 (CHead x4 k x5)
190 H6) in (eq_ind_r C (CHead x4 k x5) (\lambda (c1: C).(eq C c1 (CHead x0 k
191 x3))) (let H10 \def (eq_ind T t (\lambda (t: T).(\forall (h: nat).((drop h n
192 (CHead c0 k t) (CHead x4 k x5)) \to (\forall (x2: C).((drop h n (CHead c0 k
193 t) x2) \to (eq C (CHead x4 k x5) x2)))))) H9 (lift h (r k n) x5) H7) in (let
194 H11 \def (eq_ind T t (\lambda (t: T).(eq T t (lift h (r k n) x3))) H4 (lift h
195 (r k n) x5) H7) in (let H12 \def (eq_ind T x5 (\lambda (t: T).(\forall (h0:
196 nat).((drop h0 n (CHead c0 k (lift h (r k n) t)) (CHead x4 k t)) \to (\forall
197 (x2: C).((drop h0 n (CHead c0 k (lift h (r k n) t)) x2) \to (eq C (CHead x4 k
198 t) x2)))))) H10 x3 (lift_inj x5 x3 h (r k n) H11)) in (eq_ind_r T x3 (\lambda
199 (t0: T).(eq C (CHead x4 k t0) (CHead x0 k x3))) (sym_equal C (CHead x0 k x3)
200 (CHead x4 k x3) (sym_equal C (CHead x4 k x3) (CHead x0 k x3) (sym_equal C
201 (CHead x0 k x3) (CHead x4 k x3) (f_equal3 C K T C CHead x0 x4 k k x3 x3 (H x0
202 (r k n) h H5 x4 H8) (refl_equal K k) (refl_equal T x3))))) x5 (lift_inj x5 x3
203 h (r k n) H11))))) x1 H6)) x2 H3)))))) (drop_gen_skip_l c0 x1 t h n k
204 H1))))))) (drop_gen_skip_l c0 x2 t h n k H2)))))))) d))))))) c).
206 theorem drop_conf_lt:
207 \forall (k: K).(\forall (i: nat).(\forall (u: T).(\forall (c0: C).(\forall
208 (c: C).((drop i O c (CHead c0 k u)) \to (\forall (e: C).(\forall (h:
209 nat).(\forall (d: nat).((drop h (S (plus i d)) c e) \to (ex3_2 T C (\lambda
210 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
211 (e0: C).(drop i O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop
212 h (r k d) c0 e0)))))))))))))
214 \lambda (k: K).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (u:
215 T).(\forall (c0: C).(\forall (c: C).((drop n O c (CHead c0 k u)) \to (\forall
216 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus n d)) c e) \to
217 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v))))
218 (\lambda (v: T).(\lambda (e0: C).(drop n O e (CHead e0 k v)))) (\lambda (_:
219 T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))))) (\lambda (u:
220 T).(\lambda (c0: C).(\lambda (c: C).(\lambda (H: (drop O O c (CHead c0 k
221 u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop
222 h (S (plus O d)) c e)).(let H1 \def (eq_ind C c (\lambda (c: C).(drop h (S
223 (plus O d)) c e)) H0 (CHead c0 k u) (drop_gen_refl c (CHead c0 k u) H)) in
224 (ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 k v))))
225 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k (plus O d)) v))))
226 (\lambda (e0: C).(\lambda (_: T).(drop h (r k (plus O d)) c0 e0))) (ex3_2 T C
227 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
228 T).(\lambda (e0: C).(drop O O e (CHead e0 k v)))) (\lambda (_: T).(\lambda
229 (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda
230 (H2: (eq C e (CHead x0 k x1))).(\lambda (H3: (eq T u (lift h (r k (plus O d))
231 x1))).(\lambda (H4: (drop h (r k (plus O d)) c0 x0)).(eq_ind_r C (CHead x0 k
232 x1) (\lambda (c1: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift
233 h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop O O c1 (CHead e0 k
234 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))) (eq_ind_r T
235 (lift h (r k (plus O d)) x1) (\lambda (t: T).(ex3_2 T C (\lambda (v:
236 T).(\lambda (_: C).(eq T t (lift h (r k d) v)))) (\lambda (v: T).(\lambda
237 (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda
238 (e0: C).(drop h (r k d) c0 e0))))) (ex3_2_intro T C (\lambda (v: T).(\lambda
239 (_: C).(eq T (lift h (r k (plus O d)) x1) (lift h (r k d) v)))) (\lambda (v:
240 T).(\lambda (e0: C).(drop O O (CHead x0 k x1) (CHead e0 k v)))) (\lambda (_:
241 T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x1 x0 (refl_equal T (lift h (r k
242 d) x1)) (drop_refl (CHead x0 k x1)) H4) u H3) e H2)))))) (drop_gen_skip_l c0
243 e u h (plus O d) k H1))))))))))) (\lambda (i0: nat).(\lambda (H: ((\forall
244 (u: T).(\forall (c0: C).(\forall (c: C).((drop i0 O c (CHead c0 k u)) \to
245 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus i0 d))
246 c e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
247 v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O e (CHead e0 k v))))
248 (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))))))))))))).(\lambda
249 (u: T).(\lambda (c0: C).(\lambda (c: C).(C_ind (\lambda (c1: C).((drop (S i0)
250 O c1 (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
251 nat).((drop h (S (plus (S i0) d)) c1 e) \to (ex3_2 T C (\lambda (v:
252 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
253 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
254 C).(drop h (r k d) c0 e0)))))))))) (\lambda (n: nat).(\lambda (_: (drop (S
255 i0) O (CSort n) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda
256 (d: nat).(\lambda (H1: (drop h (S (plus (S i0) d)) (CSort n) e)).(and3_ind
257 (eq C e (CSort n)) (eq nat h O) (eq nat (S (plus (S i0) d)) O) (ex3_2 T C
258 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
259 T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_:
260 T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (_: (eq C e (CSort
261 n))).(\lambda (_: (eq nat h O)).(\lambda (H4: (eq nat (S (plus (S i0) d))
262 O)).(let H5 \def (eq_ind nat (S (plus (S i0) d)) (\lambda (ee: nat).(match ee
263 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
264 \Rightarrow True])) I O H4) in (False_ind (ex3_2 T C (\lambda (v: T).(\lambda
265 (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop
266 (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d)
267 c0 e0)))) H5))))) (drop_gen_sort n h (S (plus (S i0) d)) e H1))))))))
268 (\lambda (c1: C).(\lambda (H0: (((drop (S i0) O c1 (CHead c0 k u)) \to
269 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus (S i0)
270 d)) c1 e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k
271 d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k v))))
272 (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))))))))).(\lambda
273 (k0: K).(K_ind (\lambda (k1: K).(\forall (t: T).((drop (S i0) O (CHead c1 k1
274 t) (CHead c0 k u)) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
275 nat).((drop h (S (plus (S i0) d)) (CHead c1 k1 t) e) \to (ex3_2 T C (\lambda
276 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
277 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
278 C).(drop h (r k d) c0 e0))))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda
279 (H1: (drop (S i0) O (CHead c1 (Bind b) t) (CHead c0 k u))).(\lambda (e:
280 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0)
281 d)) (CHead c1 (Bind b) t) e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v:
282 T).(eq C e (CHead e0 (Bind b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
283 (lift h (r (Bind b) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_:
284 T).(drop h (r (Bind b) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v:
285 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
286 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
287 C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3:
288 (eq C e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b)
289 (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Bind b) (plus (S i0) d)) c1
290 x0)).(eq_ind_r C (CHead x0 (Bind b) x1) (\lambda (c2: C).(ex3_2 T C (\lambda
291 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
292 (e0: C).(drop (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
293 C).(drop h (r k d) c0 e0))))) (let H6 \def (H u c0 c1 (drop_gen_drop (Bind b)
294 c1 (CHead c0 k u) t i0 H1) x0 h d H5) in (ex3_2_ind T C (\lambda (v:
295 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
296 (e0: C).(drop i0 O x0 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
297 C).(drop h (r k d) c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T
298 u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O
299 (CHead x0 (Bind b) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
300 C).(drop h (r k d) c0 e0)))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H7:
301 (eq T u (lift h (r k d) x2))).(\lambda (H8: (drop i0 O x0 (CHead x3 k
302 x2))).(\lambda (H9: (drop h (r k d) c0 x3)).(ex3_2_intro T C (\lambda (v:
303 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
304 (e0: C).(drop (S i0) O (CHead x0 (Bind b) x1) (CHead e0 k v)))) (\lambda (_:
305 T).(\lambda (e0: C).(drop h (r k d) c0 e0))) x2 x3 H7 (drop_drop (Bind b) i0
306 x0 (CHead x3 k x2) H8 x1) H9)))))) H6)) e H3)))))) (drop_gen_skip_l c1 e t h
307 (plus (S i0) d) (Bind b) H2))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda
308 (H1: (drop (S i0) O (CHead c1 (Flat f) t) (CHead c0 k u))).(\lambda (e:
309 C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h (S (plus (S i0)
310 d)) (CHead c1 (Flat f) t) e)).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v:
311 T).(eq C e (CHead e0 (Flat f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t
312 (lift h (r (Flat f) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_:
313 T).(drop h (r (Flat f) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v:
314 T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
315 (e0: C).(drop (S i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
316 C).(drop h (r k d) c0 e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3:
317 (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f)
318 (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Flat f) (plus (S i0) d)) c1
319 x0)).(eq_ind_r C (CHead x0 (Flat f) x1) (\lambda (c2: C).(ex3_2 T C (\lambda
320 (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda
321 (e0: C).(drop (S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0:
322 C).(drop h (r k d) c0 e0))))) (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
323 C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S
324 i0) O x0 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d)
325 c0 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
326 v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1)
327 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))
328 (\lambda (x2: T).(\lambda (x3: C).(\lambda (H6: (eq T u (lift h (r k d)
329 x2))).(\lambda (H7: (drop (S i0) O x0 (CHead x3 k x2))).(\lambda (H8: (drop h
330 (r k d) c0 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u
331 (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead
332 x0 (Flat f) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r
333 k d) c0 e0))) x2 x3 H6 (drop_drop (Flat f) i0 x0 (CHead x3 k x2) H7 x1)
334 H8)))))) (H0 (drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e
335 H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2)))))))))
338 theorem drop_conf_ge:
339 \forall (i: nat).(\forall (a: C).(\forall (c: C).((drop i O c a) \to
340 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le
341 (plus d h) i) \to (drop (minus i h) O e a)))))))))
343 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (a: C).(\forall (c:
344 C).((drop n O c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
345 nat).((drop h d c e) \to ((le (plus d h) n) \to (drop (minus n h) O e
346 a)))))))))) (\lambda (a: C).(\lambda (c: C).(\lambda (H: (drop O O c
347 a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h
348 d c e)).(\lambda (H1: (le (plus d h) O)).(let H2 \def (eq_ind C c (\lambda
349 (c: C).(drop h d c e)) H0 a (drop_gen_refl c a H)) in (let H3 \def (match H1
350 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) \to (drop
351 (minus O h) O e a)))) with [le_n \Rightarrow (\lambda (H: (eq nat (plus d h)
352 O)).(let H3 \def (f_equal nat nat (\lambda (e0: nat).e0) (plus d h) O H) in
353 (eq_ind nat (plus d h) (\lambda (n: nat).(drop (minus n h) n e a)) (eq_ind_r
354 nat O (\lambda (n: nat).(drop (minus n h) n e a)) (and_ind (eq nat d O) (eq
355 nat h O) (drop O O e a) (\lambda (H0: (eq nat d O)).(\lambda (H1: (eq nat h
356 O)).(let H2 \def (eq_ind nat d (\lambda (n: nat).(drop h n a e)) H2 O H0) in
357 (let H4 \def (eq_ind nat h (\lambda (n: nat).(drop n O a e)) H2 O H1) in
358 (eq_ind C a (\lambda (c: C).(drop O O c a)) (drop_refl a) e (drop_gen_refl a
359 e H4)))))) (plus_O d h H3)) (plus d h) H3) O H3))) | (le_S m H) \Rightarrow
360 (\lambda (H2: (eq nat (S m) O)).((let H0 \def (eq_ind nat (S m) (\lambda (e0:
361 nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
362 False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (plus d h) m)
363 \to (drop (minus O h) O e a)) H0)) H))]) in (H3 (refl_equal nat O))))))))))))
364 (\lambda (i0: nat).(\lambda (H: ((\forall (a: C).(\forall (c: C).((drop i0 O
365 c a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e)
366 \to ((le (plus d h) i0) \to (drop (minus i0 h) O e a))))))))))).(\lambda (a:
367 C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop (S i0) O c0 a) \to (\forall
368 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d
369 h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))) (\lambda (n:
370 nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda (h:
371 nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda (H2:
372 (le (plus d h) (S i0))).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat d
373 O) (drop (minus (S i0) h) O e a) (\lambda (H3: (eq C e (CSort n))).(\lambda
374 (H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(and3_ind (eq C a (CSort n))
375 (eq nat (S i0) O) (eq nat O O) (drop (minus (S i0) h) O e a) (\lambda (H6:
376 (eq C a (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O
377 O)).(let H9 \def (eq_ind nat d (\lambda (n: nat).(le (plus n h) (S i0))) H2 O
378 H5) in (let H10 \def (eq_ind nat h (\lambda (n: nat).(le (plus O n) (S i0)))
379 H9 O H4) in (eq_ind_r nat O (\lambda (n0: nat).(drop (minus (S i0) n0) O e
380 a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O c0 a))
381 (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O (CSort n)
382 c0)) (let H11 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat
383 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
384 True])) I O H7) in (False_ind (drop (minus (S i0) O) O (CSort n) (CSort n))
385 H11)) a H6) e H3) h H4)))))) (drop_gen_sort n (S i0) O a H0)))))
386 (drop_gen_sort n h d e H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S
387 i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
388 d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
389 a))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S
390 i0) O (CHead c0 k0 t) a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
391 nat).((drop h d (CHead c0 k0 t) e) \to ((le (plus d h) (S i0)) \to (drop
392 (minus (S i0) h) O e a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1:
393 (drop (S i0) O (CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h:
394 nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t)
395 e)).(\lambda (H3: (le (plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h
396 n (CHead c0 (Bind b) t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S
397 i0) h) O e a)))) (\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda
398 (H5: (le (plus O h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0
399 (Bind b) t) e) \to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e
400 a)))) (\lambda (H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le
401 (plus O O) (S i0))).(eq_ind C (CHead c0 (Bind b) t) (\lambda (c1: C).(drop
402 (minus (S i0) O) O c1 a)) (drop_drop (Bind b) i0 c0 a (drop_gen_drop (Bind b)
403 c0 a t i0 H1) t) e (drop_gen_refl (CHead c0 (Bind b) t) e H6)))) (\lambda
404 (h0: nat).(\lambda (_: (((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O
405 h0) (S i0)) \to (drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0)
406 O (CHead c0 (Bind b) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H a
407 c0 (drop_gen_drop (Bind b) c0 a t i0 H1) e h0 O (drop_gen_drop (Bind b) c0 e
408 t h0 H6) (le_S_n (plus O h0) i0 H7)))))) h H4 H5))) (\lambda (d0:
409 nat).(\lambda (_: (((drop h d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h)
410 (S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
411 (CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
412 i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Bind
413 b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0)
414 v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Bind b) d0) c0 e0))) (drop
415 (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
416 e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) d0)
417 x1))).(\lambda (H8: (drop h (r (Bind b) d0) c0 x0)).(eq_ind_r C (CHead x0
418 (Bind b) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (eq_ind nat (S
419 (minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Bind b) x1) a))
420 (drop_drop (Bind b) (minus i0 h) x0 a (H a c0 (drop_gen_drop (Bind b) c0 a t
421 i0 H1) x0 h d0 H8 (le_S_n (plus d0 h) i0 H5)) x1) (minus (S i0) h)
422 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) e
423 H6)))))) (drop_gen_skip_l c0 e t h d0 (Bind b) H4)))))) d H2 H3)))))))))
424 (\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c0 (Flat
425 f) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2:
426 (drop h d (CHead c0 (Flat f) t) e)).(\lambda (H3: (le (plus d h) (S
427 i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Flat f) t) e) \to ((le
428 (plus n h) (S i0)) \to (drop (minus (S i0) h) O e a)))) (\lambda (H4: (drop h
429 O (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus O h) (S i0))).(nat_ind
430 (\lambda (n: nat).((drop n O (CHead c0 (Flat f) t) e) \to ((le (plus O n) (S
431 i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda (H6: (drop O O (CHead c0
432 (Flat f) t) e)).(\lambda (_: (le (plus O O) (S i0))).(eq_ind C (CHead c0
433 (Flat f) t) (\lambda (c1: C).(drop (minus (S i0) O) O c1 a)) (drop_drop (Flat
434 f) i0 c0 a (drop_gen_drop (Flat f) c0 a t i0 H1) t) e (drop_gen_refl (CHead
435 c0 (Flat f) t) e H6)))) (\lambda (h0: nat).(\lambda (_: (((drop h0 O (CHead
436 c0 (Flat f) t) e) \to ((le (plus O h0) (S i0)) \to (drop (minus (S i0) h0) O
437 e a))))).(\lambda (H6: (drop (S h0) O (CHead c0 (Flat f) t) e)).(\lambda (H7:
438 (le (plus O (S h0)) (S i0))).(H0 (drop_gen_drop (Flat f) c0 a t i0 H1) e (S
439 h0) O (drop_gen_drop (Flat f) c0 e t h0 H6) H7))))) h H4 H5))) (\lambda (d0:
440 nat).(\lambda (_: (((drop h d0 (CHead c0 (Flat f) t) e) \to ((le (plus d0 h)
441 (S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
442 (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
443 i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Flat
444 f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0)
445 v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) d0) c0 e0))) (drop
446 (minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
447 e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t (lift h (r (Flat f) d0)
448 x1))).(\lambda (H8: (drop h (r (Flat f) d0) c0 x0)).(eq_ind_r C (CHead x0
449 (Flat f) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (let H9 \def
450 (eq_ind_r nat (minus (S i0) h) (\lambda (n: nat).(drop n O x0 a)) (H0
451 (drop_gen_drop (Flat f) c0 a t i0 H1) x0 h (S d0) H8 H5) (S (minus i0 h))
452 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) in
453 (eq_ind nat (S (minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Flat f)
454 x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 x1) (minus (S i0) h)
455 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5))))) e
456 H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2 H3)))))))))
459 theorem drop_conf_rev:
460 \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
461 (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1:
462 C).(drop j O c1 c2)) (\lambda (c1: C).(drop i j c1 e1)))))))))
464 \lambda (j: nat).(nat_ind (\lambda (n: nat).(\forall (e1: C).(\forall (e2:
465 C).((drop n O e1 e2) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e2)
466 \to (ex2 C (\lambda (c1: C).(drop n O c1 c2)) (\lambda (c1: C).(drop i n c1
467 e1)))))))))) (\lambda (e1: C).(\lambda (e2: C).(\lambda (H: (drop O O e1
468 e2)).(\lambda (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(let
469 H1 \def (eq_ind_r C e2 (\lambda (c: C).(drop i O c2 c)) H0 e1 (drop_gen_refl
470 e1 e2 H)) in (ex_intro2 C (\lambda (c1: C).(drop O O c1 c2)) (\lambda (c1:
471 C).(drop i O c1 e1)) c2 (drop_refl c2) H1)))))))) (\lambda (j0: nat).(\lambda
472 (IHj: ((\forall (e1: C).(\forall (e2: C).((drop j0 O e1 e2) \to (\forall (c2:
473 C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop j0 O
474 c1 c2)) (\lambda (c1: C).(drop i j0 c1 e1))))))))))).(\lambda (e1: C).(C_ind
475 (\lambda (c: C).(\forall (e2: C).((drop (S j0) O c e2) \to (\forall (c2:
476 C).(\forall (i: nat).((drop i O c2 e2) \to (ex2 C (\lambda (c1: C).(drop (S
477 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 c))))))))) (\lambda (n:
478 nat).(\lambda (e2: C).(\lambda (H: (drop (S j0) O (CSort n) e2)).(\lambda
479 (c2: C).(\lambda (i: nat).(\lambda (H0: (drop i O c2 e2)).(and3_ind (eq C e2
480 (CSort n)) (eq nat (S j0) O) (eq nat O O) (ex2 C (\lambda (c1: C).(drop (S
481 j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) (\lambda (H1:
482 (eq C e2 (CSort n))).(\lambda (H2: (eq nat (S j0) O)).(\lambda (_: (eq nat O
483 O)).(let H4 \def (eq_ind C e2 (\lambda (c: C).(drop i O c2 c)) H0 (CSort n)
484 H1) in (let H5 \def (eq_ind nat (S j0) (\lambda (ee: nat).(match ee in nat
485 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
486 True])) I O H2) in (False_ind (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2))
487 (\lambda (c1: C).(drop i (S j0) c1 (CSort n)))) H5)))))) (drop_gen_sort n (S
488 j0) O e2 H)))))))) (\lambda (e2: C).(\lambda (IHe1: ((\forall (e3: C).((drop
489 (S j0) O e2 e3) \to (\forall (c2: C).(\forall (i: nat).((drop i O c2 e3) \to
490 (ex2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S
491 j0) c1 e2)))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e3: C).(\lambda
492 (H: (drop (S j0) O (CHead e2 k t) e3)).(\lambda (c2: C).(\lambda (i:
493 nat).(\lambda (H0: (drop i O c2 e3)).((match k in K return (\lambda (k0:
494 K).((drop (r k0 j0) O e2 e3) \to (ex2 C (\lambda (c1: C).(drop (S j0) O c1
495 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 k0 t)))))) with [(Bind b)
496 \Rightarrow (\lambda (H1: (drop (r (Bind b) j0) O e2 e3)).(let H_x \def (IHj
497 e2 e3 H1 c2 i H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c1: C).(drop j0
498 O c1 c2)) (\lambda (c1: C).(drop i j0 c1 e2)) (ex2 C (\lambda (c1: C).(drop
499 (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Bind b) t))))
500 (\lambda (x: C).(\lambda (H3: (drop j0 O x c2)).(\lambda (H4: (drop i j0 x
501 e2)).(ex_intro2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1:
502 C).(drop i (S j0) c1 (CHead e2 (Bind b) t))) (CHead x (Bind b) (lift i (r
503 (Bind b) j0) t)) (drop_drop (Bind b) j0 x c2 H3 (lift i (r (Bind b) j0) t))
504 (drop_skip (Bind b) i j0 x e2 H4 t))))) H2)))) | (Flat f) \Rightarrow
505 (\lambda (H1: (drop (r (Flat f) j0) O e2 e3)).(let H_x \def (IHe1 e3 H1 c2 i
506 H0) in (let H2 \def H_x in (ex2_ind C (\lambda (c1: C).(drop (S j0) O c1 c2))
507 (\lambda (c1: C).(drop i (S j0) c1 e2)) (ex2 C (\lambda (c1: C).(drop (S j0)
508 O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat f) t))))
509 (\lambda (x: C).(\lambda (H3: (drop (S j0) O x c2)).(\lambda (H4: (drop i (S
510 j0) x e2)).(ex_intro2 C (\lambda (c1: C).(drop (S j0) O c1 c2)) (\lambda (c1:
511 C).(drop i (S j0) c1 (CHead e2 (Flat f) t))) (CHead x (Flat f) (lift i (r
512 (Flat f) j0) t)) (drop_drop (Flat f) j0 x c2 H3 (lift i (r (Flat f) j0) t))
513 (drop_skip (Flat f) i j0 x e2 H4 t))))) H2))))]) (drop_gen_drop k e2 e3 t j0
514 H))))))))))) e1)))) j).
516 theorem drop_trans_le:
517 \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall
518 (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O
519 c2 e2) \to (ex2 C (\lambda (e1: C).(drop i O c1 e1)) (\lambda (e1: C).(drop h
520 (minus d i) e1 e2)))))))))))
522 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (d: nat).((le n d) \to
523 (\forall (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to
524 (\forall (e2: C).((drop n O c2 e2) \to (ex2 C (\lambda (e1: C).(drop n O c1
525 e1)) (\lambda (e1: C).(drop h (minus d n) e1 e2)))))))))))) (\lambda (d:
526 nat).(\lambda (_: (le O d)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h:
527 nat).(\lambda (H0: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H1: (drop O O
528 c2 e2)).(let H2 \def (eq_ind C c2 (\lambda (c: C).(drop h d c1 c)) H0 e2
529 (drop_gen_refl c2 e2 H1)) in (eq_ind nat d (\lambda (n: nat).(ex2 C (\lambda
530 (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h n e1 e2)))) (ex_intro2 C
531 (\lambda (e1: C).(drop O O c1 e1)) (\lambda (e1: C).(drop h d e1 e2)) c1
532 (drop_refl c1) H2) (minus d O) (minus_n_O d))))))))))) (\lambda (i0:
533 nat).(\lambda (IHi: ((\forall (d: nat).((le i0 d) \to (\forall (c1:
534 C).(\forall (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2:
535 C).((drop i0 O c2 e2) \to (ex2 C (\lambda (e1: C).(drop i0 O c1 e1)) (\lambda
536 (e1: C).(drop h (minus d i0) e1 e2))))))))))))).(\lambda (d: nat).(nat_ind
537 (\lambda (n: nat).((le (S i0) n) \to (\forall (c1: C).(\forall (c2:
538 C).(\forall (h: nat).((drop h n c1 c2) \to (\forall (e2: C).((drop (S i0) O
539 c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
540 C).(drop h (minus n (S i0)) e1 e2))))))))))) (\lambda (H: (le (S i0)
541 O)).(\lambda (c1: C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (_: (drop h
542 O c1 c2)).(\lambda (e2: C).(\lambda (_: (drop (S i0) O c2 e2)).(let H2 \def
543 (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O)
544 \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1: C).(drop h
545 (minus O (S i0)) e1 e2)))))) with [le_n \Rightarrow (\lambda (H2: (eq nat (S
546 i0) O)).(let H3 \def (eq_ind nat (S i0) (\lambda (e: nat).(match e in nat
547 return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
548 True])) I O H2) in (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1))
549 (\lambda (e1: C).(drop h (minus O (S i0)) e1 e2))) H3))) | (le_S m H2)
550 \Rightarrow (\lambda (H3: (eq nat (S m) O)).((let H4 \def (eq_ind nat (S m)
551 (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O
552 \Rightarrow False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S
553 i0) m) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1 e1)) (\lambda (e1:
554 C).(drop h (minus O (S i0)) e1 e2)))) H4)) H2))]) in (H2 (refl_equal nat
555 O)))))))))) (\lambda (d0: nat).(\lambda (_: (((le (S i0) d0) \to (\forall
556 (c1: C).(\forall (c2: C).(\forall (h: nat).((drop h d0 c1 c2) \to (\forall
557 (e2: C).((drop (S i0) O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c1
558 e1)) (\lambda (e1: C).(drop h (minus d0 (S i0)) e1 e2)))))))))))).(\lambda
559 (H: (le (S i0) (S d0))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2:
560 C).(\forall (h: nat).((drop h (S d0) c c2) \to (\forall (e2: C).((drop (S i0)
561 O c2 e2) \to (ex2 C (\lambda (e1: C).(drop (S i0) O c e1)) (\lambda (e1:
562 C).(drop h (minus (S d0) (S i0)) e1 e2))))))))) (\lambda (n: nat).(\lambda
563 (c2: C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CSort n)
564 c2)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c2 e2)).(and3_ind (eq C c2
565 (CSort n)) (eq nat h O) (eq nat (S d0) O) (ex2 C (\lambda (e1: C).(drop (S
566 i0) O (CSort n) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)))
567 (\lambda (H2: (eq C c2 (CSort n))).(\lambda (_: (eq nat h O)).(\lambda (_:
568 (eq nat (S d0) O)).(let H5 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c
569 e2)) H1 (CSort n) H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq
570 nat O O) (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda (e1:
571 C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (H6: (eq C e2 (CSort
572 n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C
573 (CSort n) (\lambda (c: C).(ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n)
574 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 c)))) (let H9 \def
575 (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat return (\lambda (_:
576 nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H7) in
577 (False_ind (ex2 C (\lambda (e1: C).(drop (S i0) O (CSort n) e1)) (\lambda
578 (e1: C).(drop h (minus (S d0) (S i0)) e1 (CSort n)))) H9)) e2 H6))))
579 (drop_gen_sort n (S i0) O e2 H5)))))) (drop_gen_sort n h (S d0) c2 H0))))))))
580 (\lambda (c2: C).(\lambda (IHc: ((\forall (c3: C).(\forall (h: nat).((drop h
581 (S d0) c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda
582 (e1: C).(drop (S i0) O c2 e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0))
583 e1 e2)))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t:
584 T).(\forall (c3: C).(\forall (h: nat).((drop h (S d0) (CHead c2 k0 t) c3) \to
585 (\forall (e2: C).((drop (S i0) O c3 e2) \to (ex2 C (\lambda (e1: C).(drop (S
586 i0) O (CHead c2 k0 t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
587 e2)))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (c3: C).(\lambda (h:
588 nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Bind b) t) c3)).(\lambda (e2:
589 C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T (\lambda (e:
590 C).(\lambda (v: T).(eq C c3 (CHead e (Bind b) v)))) (\lambda (_: C).(\lambda
591 (v: T).(eq T t (lift h (r (Bind b) d0) v)))) (\lambda (e: C).(\lambda (_:
592 T).(drop h (r (Bind b) d0) c2 e))) (ex2 C (\lambda (e1: C).(drop (S i0) O
593 (CHead c2 (Bind b) t) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
594 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3 (CHead x0
595 (Bind b) x1))).(\lambda (H3: (eq T t (lift h (r (Bind b) d0) x1))).(\lambda
596 (H4: (drop h (r (Bind b) d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c:
597 C).(drop (S i0) O c e2)) H1 (CHead x0 (Bind b) x1) H2) in (eq_ind_r T (lift h
598 (r (Bind b) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1: C).(drop (S i0) O
599 (CHead c2 (Bind b) t0) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1
600 e2)))) (ex2_ind C (\lambda (e1: C).(drop i0 O c2 e1)) (\lambda (e1: C).(drop
601 h (minus d0 i0) e1 e2)) (ex2 C (\lambda (e1: C).(drop (S i0) O (CHead c2
602 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S
603 d0) (S i0)) e1 e2))) (\lambda (x: C).(\lambda (H6: (drop i0 O c2 x)).(\lambda
604 (H7: (drop h (minus d0 i0) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0)
605 O (CHead c2 (Bind b) (lift h (r (Bind b) d0) x1)) e1)) (\lambda (e1: C).(drop
606 h (minus (S d0) (S i0)) e1 e2)) x (drop_drop (Bind b) i0 c2 x H6 (lift h (r
607 (Bind b) d0) x1)) H7)))) (IHi d0 (le_S_n i0 d0 H) c2 x0 h H4 e2
608 (drop_gen_drop (Bind b) x0 e2 x1 i0 H5))) t H3))))))) (drop_gen_skip_l c2 c3
609 t h d0 (Bind b) H0))))))))) (\lambda (f: F).(\lambda (t: T).(\lambda (c3:
610 C).(\lambda (h: nat).(\lambda (H0: (drop h (S d0) (CHead c2 (Flat f) t)
611 c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(ex3_2_ind C T
612 (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e (Flat f) v)))) (\lambda (_:
613 C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0) v)))) (\lambda (e:
614 C).(\lambda (_: T).(drop h (r (Flat f) d0) c2 e))) (ex2 C (\lambda (e1:
615 C).(drop (S i0) O (CHead c2 (Flat f) t) e1)) (\lambda (e1: C).(drop h (minus
616 (S d0) (S i0)) e1 e2))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C
617 c3 (CHead x0 (Flat f) x1))).(\lambda (H3: (eq T t (lift h (r (Flat f) d0)
618 x1))).(\lambda (H4: (drop h (r (Flat f) d0) c2 x0)).(let H5 \def (eq_ind C c3
619 (\lambda (c: C).(drop (S i0) O c e2)) H1 (CHead x0 (Flat f) x1) H2) in
620 (eq_ind_r T (lift h (r (Flat f) d0) x1) (\lambda (t0: T).(ex2 C (\lambda (e1:
621 C).(drop (S i0) O (CHead c2 (Flat f) t0) e1)) (\lambda (e1: C).(drop h (minus
622 (S d0) (S i0)) e1 e2)))) (ex2_ind C (\lambda (e1: C).(drop (S i0) O c2 e1))
623 (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2)) (ex2 C (\lambda (e1:
624 C).(drop (S i0) O (CHead c2 (Flat f) (lift h (r (Flat f) d0) x1)) e1))
625 (\lambda (e1: C).(drop h (minus (S d0) (S i0)) e1 e2))) (\lambda (x:
626 C).(\lambda (H6: (drop (S i0) O c2 x)).(\lambda (H7: (drop h (minus (S d0) (S
627 i0)) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f)
628 (lift h (r (Flat f) d0) x1)) e1)) (\lambda (e1: C).(drop h (minus (S d0) (S
629 i0)) e1 e2)) x (drop_drop (Flat f) i0 c2 x H6 (lift h (r (Flat f) d0) x1))
630 H7)))) (IHc x0 h H4 e2 (drop_gen_drop (Flat f) x0 e2 x1 i0 H5))) t H3)))))))
631 (drop_gen_skip_l c2 c3 t h d0 (Flat f) H0))))))))) k)))) c1))))) d)))) i).
633 theorem drop_trans_ge:
634 \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d:
635 nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((drop i O c2
636 e2) \to ((le d i) \to (drop (plus i h) O c1 e2)))))))))
638 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c2:
639 C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2:
640 C).((drop n O c2 e2) \to ((le d n) \to (drop (plus n h) O c1 e2))))))))))
641 (\lambda (c1: C).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
642 nat).(\lambda (H: (drop h d c1 c2)).(\lambda (e2: C).(\lambda (H0: (drop O O
643 c2 e2)).(\lambda (H1: (le d O)).(eq_ind C c2 (\lambda (c: C).(drop (plus O h)
644 O c1 c)) (let H2 \def (match H1 in le return (\lambda (n: nat).(\lambda (_:
645 (le ? n)).((eq nat n O) \to (drop (plus O h) O c1 c2)))) with [le_n
646 \Rightarrow (\lambda (H0: (eq nat d O)).(eq_ind nat O (\lambda (_: nat).(drop
647 (plus O h) O c1 c2)) (let H2 \def (eq_ind nat d (\lambda (n: nat).(le n O))
648 H1 O H0) in (let H3 \def (eq_ind nat d (\lambda (n: nat).(drop h n c1 c2)) H
649 O H0) in H3)) d (sym_eq nat d O H0))) | (le_S m H0) \Rightarrow (\lambda (H2:
650 (eq nat (S m) O)).((let H1 \def (eq_ind nat (S m) (\lambda (e: nat).(match e
651 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
652 \Rightarrow True])) I O H2) in (False_ind ((le d m) \to (drop (plus O h) O c1
653 c2)) H1)) H0))]) in (H2 (refl_equal nat O))) e2 (drop_gen_refl c2 e2
654 H0)))))))))) (\lambda (i0: nat).(\lambda (IHi: ((\forall (c1: C).(\forall
655 (c2: C).(\forall (d: nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall
656 (e2: C).((drop i0 O c2 e2) \to ((le d i0) \to (drop (plus i0 h) O c1
657 e2))))))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2:
658 C).(\forall (d: nat).(\forall (h: nat).((drop h d c c2) \to (\forall (e2:
659 C).((drop (S i0) O c2 e2) \to ((le d (S i0)) \to (drop (plus (S i0) h) O c
660 e2))))))))) (\lambda (n: nat).(\lambda (c2: C).(\lambda (d: nat).(\lambda (h:
661 nat).(\lambda (H: (drop h d (CSort n) c2)).(\lambda (e2: C).(\lambda (H0:
662 (drop (S i0) O c2 e2)).(\lambda (H1: (le d (S i0))).(and3_ind (eq C c2 (CSort
663 n)) (eq nat h O) (eq nat d O) (drop (S (plus i0 h)) O (CSort n) e2) (\lambda
664 (H2: (eq C c2 (CSort n))).(\lambda (H3: (eq nat h O)).(\lambda (H4: (eq nat d
665 O)).(eq_ind_r nat O (\lambda (n0: nat).(drop (S (plus i0 n0)) O (CSort n)
666 e2)) (let H5 \def (eq_ind nat d (\lambda (n: nat).(le n (S i0))) H1 O H4) in
667 (let H6 \def (eq_ind C c2 (\lambda (c: C).(drop (S i0) O c e2)) H0 (CSort n)
668 H2) in (and3_ind (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O) (drop (S
669 (plus i0 O)) O (CSort n) e2) (\lambda (H7: (eq C e2 (CSort n))).(\lambda (H8:
670 (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(eq_ind_r C (CSort n) (\lambda
671 (c: C).(drop (S (plus i0 O)) O (CSort n) c)) (let H10 \def (eq_ind nat (S i0)
672 (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
673 \Rightarrow False | (S _) \Rightarrow True])) I O H8) in (False_ind (drop (S
674 (plus i0 O)) O (CSort n) (CSort n)) H10)) e2 H7)))) (drop_gen_sort n (S i0) O
675 e2 H6)))) h H3)))) (drop_gen_sort n h d c2 H)))))))))) (\lambda (c2:
676 C).(\lambda (IHc: ((\forall (c3: C).(\forall (d: nat).(\forall (h:
677 nat).((drop h d c2 c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le d
678 (S i0)) \to (drop (S (plus i0 h)) O c2 e2)))))))))).(\lambda (k: K).(\lambda
679 (t: T).(\lambda (c3: C).(\lambda (d: nat).(nat_ind (\lambda (n: nat).(\forall
680 (h: nat).((drop h n (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O
681 c3 e2) \to ((le n (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t)
682 e2))))))) (\lambda (h: nat).(nat_ind (\lambda (n: nat).((drop n O (CHead c2 k
683 t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le O (S i0)) \to
684 (drop (S (plus i0 n)) O (CHead c2 k t) e2)))))) (\lambda (H: (drop O O (CHead
685 c2 k t) c3)).(\lambda (e2: C).(\lambda (H0: (drop (S i0) O c3 e2)).(\lambda
686 (_: (le O (S i0))).(let H2 \def (eq_ind_r C c3 (\lambda (c: C).(drop (S i0) O
687 c e2)) H0 (CHead c2 k t) (drop_gen_refl (CHead c2 k t) c3 H)) in (eq_ind nat
688 i0 (\lambda (n: nat).(drop (S n) O (CHead c2 k t) e2)) (drop_drop k i0 c2 e2
689 (drop_gen_drop k c2 e2 t i0 H2) t) (plus i0 O) (plus_n_O i0))))))) (\lambda
690 (n: nat).(\lambda (_: (((drop n O (CHead c2 k t) c3) \to (\forall (e2:
691 C).((drop (S i0) O c3 e2) \to ((le O (S i0)) \to (drop (S (plus i0 n)) O
692 (CHead c2 k t) e2))))))).(\lambda (H0: (drop (S n) O (CHead c2 k t)
693 c3)).(\lambda (e2: C).(\lambda (H1: (drop (S i0) O c3 e2)).(\lambda (H2: (le
694 O (S i0))).(eq_ind nat (S (plus i0 n)) (\lambda (n0: nat).(drop (S n0) O
695 (CHead c2 k t) e2)) (drop_drop k (S (plus i0 n)) c2 e2 (eq_ind_r nat (S (r k
696 (plus i0 n))) (\lambda (n0: nat).(drop n0 O c2 e2)) (eq_ind_r nat (plus i0 (r
697 k n)) (\lambda (n0: nat).(drop (S n0) O c2 e2)) (IHc c3 O (r k n)
698 (drop_gen_drop k c2 c3 t n H0) e2 H1 H2) (r k (plus i0 n)) (r_plus_sym k i0
699 n)) (r k (S (plus i0 n))) (r_S k (plus i0 n))) t) (plus i0 (S n)) (plus_n_Sm
700 i0 n)))))))) h)) (\lambda (d0: nat).(\lambda (IHd: ((\forall (h: nat).((drop
701 h d0 (CHead c2 k t) c3) \to (\forall (e2: C).((drop (S i0) O c3 e2) \to ((le
702 d0 (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2)))))))).(\lambda (h:
703 nat).(\lambda (H: (drop h (S d0) (CHead c2 k t) c3)).(\lambda (e2:
704 C).(\lambda (H0: (drop (S i0) O c3 e2)).(\lambda (H1: (le (S d0) (S
705 i0))).(ex3_2_ind C T (\lambda (e: C).(\lambda (v: T).(eq C c3 (CHead e k
706 v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k d0) v)))) (\lambda
707 (e: C).(\lambda (_: T).(drop h (r k d0) c2 e))) (drop (S (plus i0 h)) O
708 (CHead c2 k t) e2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (eq C c3
709 (CHead x0 k x1))).(\lambda (H3: (eq T t (lift h (r k d0) x1))).(\lambda (H4:
710 (drop h (r k d0) c2 x0)).(let H5 \def (eq_ind C c3 (\lambda (c: C).(\forall
711 (h: nat).((drop h d0 (CHead c2 k t) c) \to (\forall (e2: C).((drop (S i0) O c
712 e2) \to ((le d0 (S i0)) \to (drop (S (plus i0 h)) O (CHead c2 k t) e2)))))))
713 IHd (CHead x0 k x1) H2) in (let H6 \def (eq_ind C c3 (\lambda (c: C).(drop (S
714 i0) O c e2)) H0 (CHead x0 k x1) H2) in (let H7 \def (eq_ind T t (\lambda (t:
715 T).(\forall (h: nat).((drop h d0 (CHead c2 k t) (CHead x0 k x1)) \to (\forall
716 (e2: C).((drop (S i0) O (CHead x0 k x1) e2) \to ((le d0 (S i0)) \to (drop (S
717 (plus i0 h)) O (CHead c2 k t) e2))))))) H5 (lift h (r k d0) x1) H3) in
718 (eq_ind_r T (lift h (r k d0) x1) (\lambda (t0: T).(drop (S (plus i0 h)) O
719 (CHead c2 k t0) e2)) (drop_drop k (plus i0 h) c2 e2 (K_ind (\lambda (k0:
720 K).((drop h (r k0 d0) c2 x0) \to ((drop (r k0 i0) O x0 e2) \to (drop (r k0
721 (plus i0 h)) O c2 e2)))) (\lambda (b: B).(\lambda (H8: (drop h (r (Bind b)
722 d0) c2 x0)).(\lambda (H9: (drop (r (Bind b) i0) O x0 e2)).(IHi c2 x0 (r (Bind
723 b) d0) h H8 e2 H9 (le_S_n (r (Bind b) d0) i0 H1))))) (\lambda (f: F).(\lambda
724 (H8: (drop h (r (Flat f) d0) c2 x0)).(\lambda (H9: (drop (r (Flat f) i0) O x0
725 e2)).(IHc x0 (r (Flat f) d0) h H8 e2 H9 H1)))) k H4 (drop_gen_drop k x0 e2 x1
726 i0 H6)) (lift h (r k d0) x1)) t H3))))))))) (drop_gen_skip_l c2 c3 t h d0 k
727 H))))))))) d))))))) c1)))) i).
projects / helm.git / blob