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 include "LambdaDelta-1/getl/props.ma".
19 include "LambdaDelta-1/clear/drop.ma".
22 \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h:
23 nat).((getl h c (CHead e (Bind b) u)) \to (drop (S h) O c e))))))
25 \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e:
26 C).(\forall (u: T).(\forall (h: nat).((getl h c0 (CHead e (Bind b) u)) \to
27 (drop (S h) O c0 e)))))) (\lambda (n: nat).(\lambda (e: C).(\lambda (u:
28 T).(\lambda (h: nat).(\lambda (H: (getl h (CSort n) (CHead e (Bind b)
29 u))).(getl_gen_sort n h (CHead e (Bind b) u) H (drop (S h) O (CSort n)
30 e))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e: C).(\forall (u:
31 T).(\forall (h: nat).((getl h c0 (CHead e (Bind b) u)) \to (drop (S h) O c0
32 e))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (e: C).(\lambda (u:
33 T).(\lambda (h: nat).(nat_ind (\lambda (n: nat).((getl n (CHead c0 k t)
34 (CHead e (Bind b) u)) \to (drop (S n) O (CHead c0 k t) e))) (\lambda (H0:
35 (getl O (CHead c0 k t) (CHead e (Bind b) u))).(K_ind (\lambda (k0: K).((clear
36 (CHead c0 k0 t) (CHead e (Bind b) u)) \to (drop (S O) O (CHead c0 k0 t) e)))
37 (\lambda (b0: B).(\lambda (H1: (clear (CHead c0 (Bind b0) t) (CHead e (Bind
38 b) u))).(let H2 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
39 (\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c1 _ _) \Rightarrow
40 c1])) (CHead e (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0
41 (CHead e (Bind b) u) t H1)) in ((let H3 \def (f_equal C B (\lambda (e0:
42 C).(match e0 in C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b |
43 (CHead _ k0 _) \Rightarrow (match k0 in K return (\lambda (_: K).B) with
44 [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b])])) (CHead e (Bind b) u)
45 (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e (Bind b) u) t H1)) in
46 ((let H4 \def (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda
47 (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0]))
48 (CHead e (Bind b) u) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e
49 (Bind b) u) t H1)) in (\lambda (H5: (eq B b b0)).(\lambda (H6: (eq C e
50 c0)).(eq_ind_r C c0 (\lambda (c1: C).(drop (S O) O (CHead c0 (Bind b0) t)
51 c1)) (eq_ind B b (\lambda (b1: B).(drop (S O) O (CHead c0 (Bind b1) t) c0))
52 (drop_drop (Bind b) O c0 c0 (drop_refl c0) t) b0 H5) e H6)))) H3)) H2))))
53 (\lambda (f: F).(\lambda (H1: (clear (CHead c0 (Flat f) t) (CHead e (Bind b)
54 u))).(drop_clear_O b (CHead c0 (Flat f) t) e u (clear_flat c0 (CHead e (Bind
55 b) u) (clear_gen_flat f c0 (CHead e (Bind b) u) t H1) f t) e O (drop_refl
56 e)))) k (getl_gen_O (CHead c0 k t) (CHead e (Bind b) u) H0))) (\lambda (n:
57 nat).(\lambda (_: (((getl n (CHead c0 k t) (CHead e (Bind b) u)) \to (drop (S
58 n) O (CHead c0 k t) e)))).(\lambda (H1: (getl (S n) (CHead c0 k t) (CHead e
59 (Bind b) u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0:
60 nat).(drop n0 O c0 e)) (H e u (r k n) (getl_gen_S k c0 (CHead e (Bind b) u) t
61 n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
63 theorem getl_drop_conf_lt:
64 \forall (b: B).(\forall (c: C).(\forall (c0: C).(\forall (u: T).(\forall (i:
65 nat).((getl i c (CHead c0 (Bind b) u)) \to (\forall (e: C).(\forall (h:
66 nat).(\forall (d: nat).((drop h (S (plus i d)) c e) \to (ex3_2 T C (\lambda
67 (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0:
68 C).(getl i e (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop
69 h d c0 e0)))))))))))))
71 \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (c1:
72 C).(\forall (u: T).(\forall (i: nat).((getl i c0 (CHead c1 (Bind b) u)) \to
73 (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h (S (plus i d))
74 c0 e) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
75 (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b) v)))) (\lambda
76 (_: T).(\lambda (e0: C).(drop h d c1 e0))))))))))))) (\lambda (n:
77 nat).(\lambda (c0: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H: (getl i
78 (CSort n) (CHead c0 (Bind b) u))).(\lambda (e: C).(\lambda (h: nat).(\lambda
79 (d: nat).(\lambda (_: (drop h (S (plus i d)) (CSort n) e)).(getl_gen_sort n i
80 (CHead c0 (Bind b) u) H (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
81 (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b)
82 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c0 e0)))))))))))))) (\lambda
83 (c0: C).(\lambda (H: ((\forall (c1: C).(\forall (u: T).(\forall (i:
84 nat).((getl i c0 (CHead c1 (Bind b) u)) \to (\forall (e: C).(\forall (h:
85 nat).(\forall (d: nat).((drop h (S (plus i d)) c0 e) \to (ex3_2 T C (\lambda
86 (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0:
87 C).(getl i e (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop
88 h d c1 e0)))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (c1:
89 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i (CHead c0 k t)
90 (CHead c1 (Bind b) u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
91 nat).(\lambda (H1: (drop h (S (plus i d)) (CHead c0 k t) e)).(let H2 \def
92 (getl_gen_all (CHead c0 k t) (CHead c1 (Bind b) u) i H0) in (ex2_ind C
93 (\lambda (e0: C).(drop i O (CHead c0 k t) e0)) (\lambda (e0: C).(clear e0
94 (CHead c1 (Bind b) u))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
95 (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b)
96 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0)))) (\lambda (x:
97 C).(\lambda (H3: (drop i O (CHead c0 k t) x)).(\lambda (H4: (clear x (CHead
98 c1 (Bind b) u))).(C_ind (\lambda (c2: C).((drop i O (CHead c0 k t) c2) \to
99 ((clear c2 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_:
100 C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead
101 e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0)))))))
102 (\lambda (n: nat).(\lambda (_: (drop i O (CHead c0 k t) (CSort n))).(\lambda
103 (H6: (clear (CSort n) (CHead c1 (Bind b) u))).(clear_gen_sort (CHead c1 (Bind
104 b) u) n H6 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
105 (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b) v)))) (\lambda
106 (_: T).(\lambda (e0: C).(drop h d c1 e0)))))))) (\lambda (x0: C).(\lambda
107 (IHx: (((drop i O (CHead c0 k t) x0) \to ((clear x0 (CHead c1 (Bind b) u))
108 \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
109 (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b) v)))) (\lambda
110 (_: T).(\lambda (e0: C).(drop h d c1 e0)))))))).(\lambda (k0: K).(\lambda
111 (t0: T).(\lambda (H5: (drop i O (CHead c0 k t) (CHead x0 k0 t0))).(\lambda
112 (H6: (clear (CHead x0 k0 t0) (CHead c1 (Bind b) u))).(K_ind (\lambda (k1:
113 K).((drop i O (CHead c0 k t) (CHead x0 k1 t0)) \to ((clear (CHead x0 k1 t0)
114 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
115 (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b)
116 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) (\lambda (b0:
117 B).(\lambda (H7: (drop i O (CHead c0 k t) (CHead x0 (Bind b0) t0))).(\lambda
118 (H8: (clear (CHead x0 (Bind b0) t0) (CHead c1 (Bind b) u))).(let H9 \def
119 (f_equal C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with
120 [(CSort _) \Rightarrow c1 | (CHead c2 _ _) \Rightarrow c2])) (CHead c1 (Bind
121 b) u) (CHead x0 (Bind b0) t0) (clear_gen_bind b0 x0 (CHead c1 (Bind b) u) t0
122 H8)) in ((let H10 \def (f_equal C B (\lambda (e0: C).(match e0 in C return
123 (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k1 _) \Rightarrow
124 (match k1 in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 |
125 (Flat _) \Rightarrow b])])) (CHead c1 (Bind b) u) (CHead x0 (Bind b0) t0)
126 (clear_gen_bind b0 x0 (CHead c1 (Bind b) u) t0 H8)) in ((let H11 \def
127 (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with
128 [(CSort _) \Rightarrow u | (CHead _ _ t1) \Rightarrow t1])) (CHead c1 (Bind
129 b) u) (CHead x0 (Bind b0) t0) (clear_gen_bind b0 x0 (CHead c1 (Bind b) u) t0
130 H8)) in (\lambda (H12: (eq B b b0)).(\lambda (H13: (eq C c1 x0)).(let H14
131 \def (eq_ind_r T t0 (\lambda (t1: T).(drop i O (CHead c0 k t) (CHead x0 (Bind
132 b0) t1))) H7 u H11) in (let H15 \def (eq_ind_r B b0 (\lambda (b1: B).(drop i
133 O (CHead c0 k t) (CHead x0 (Bind b1) u))) H14 b H12) in (let H16 \def
134 (eq_ind_r C x0 (\lambda (c2: C).((drop i O (CHead c0 k t) c2) \to ((clear c2
135 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
136 (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b)
137 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) IHx c1 H13) in
138 (let H17 \def (eq_ind_r C x0 (\lambda (c2: C).(drop i O (CHead c0 k t) (CHead
139 c2 (Bind b) u))) H15 c1 H13) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_:
140 C).(eq T u (lift h (r (Bind b) d) v)))) (\lambda (v: T).(\lambda (e0:
141 C).(drop i O e (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0:
142 C).(drop h (r (Bind b) d) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_:
143 C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i e (CHead
144 e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))
145 (\lambda (x1: T).(\lambda (x2: C).(\lambda (H18: (eq T u (lift h (r (Bind b)
146 d) x1))).(\lambda (H19: (drop i O e (CHead x2 (Bind b) x1))).(\lambda (H20:
147 (drop h (r (Bind b) d) c1 x2)).(let H21 \def (eq_ind T u (\lambda (t1:
148 T).((drop i O (CHead c0 k t) c1) \to ((clear c1 (CHead c1 (Bind b) t1)) \to
149 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T t1 (lift h d v)))) (\lambda
150 (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b) v)))) (\lambda (_:
151 T).(\lambda (e0: C).(drop h d c1 e0))))))) H16 (lift h (r (Bind b) d) x1)
152 H18) in (eq_ind_r T (lift h (r (Bind b) d) x1) (\lambda (t1: T).(ex3_2 T C
153 (\lambda (v: T).(\lambda (_: C).(eq T t1 (lift h d v)))) (\lambda (v:
154 T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b) v)))) (\lambda (_:
155 T).(\lambda (e0: C).(drop h d c1 e0))))) (ex3_2_intro T C (\lambda (v:
156 T).(\lambda (_: C).(eq T (lift h (r (Bind b) d) x1) (lift h d v)))) (\lambda
157 (v: T).(\lambda (e0: C).(getl i e (CHead e0 (Bind b) v)))) (\lambda (_:
158 T).(\lambda (e0: C).(drop h d c1 e0))) x1 x2 (refl_equal T (lift h d x1))
159 (getl_intro i e (CHead x2 (Bind b) x1) (CHead x2 (Bind b) x1) H19 (clear_bind
160 b x2 x1)) H20) u H18))))))) (drop_conf_lt (Bind b) i u c1 (CHead c0 k t) H17
161 e h d H1))))))))) H10)) H9))))) (\lambda (f: F).(\lambda (H7: (drop i O
162 (CHead c0 k t) (CHead x0 (Flat f) t0))).(\lambda (H8: (clear (CHead x0 (Flat
163 f) t0) (CHead c1 (Bind b) u))).(nat_ind (\lambda (n: nat).((drop h (S (plus n
164 d)) (CHead c0 k t) e) \to ((drop n O (CHead c0 k t) (CHead x0 (Flat f) t0))
165 \to ((((drop n O (CHead c0 k t) x0) \to ((clear x0 (CHead c1 (Bind b) u)) \to
166 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda
167 (v: T).(\lambda (e0: C).(getl n e (CHead e0 (Bind b) v)))) (\lambda (_:
168 T).(\lambda (e0: C).(drop h d c1 e0))))))) \to (ex3_2 T C (\lambda (v:
169 T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0:
170 C).(getl n e (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop
171 h d c1 e0)))))))) (\lambda (H9: (drop h (S (plus O d)) (CHead c0 k t)
172 e)).(\lambda (H10: (drop O O (CHead c0 k t) (CHead x0 (Flat f) t0))).(\lambda
173 (IHx0: (((drop O O (CHead c0 k t) x0) \to ((clear x0 (CHead c1 (Bind b) u))
174 \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
175 (\lambda (v: T).(\lambda (e0: C).(getl O e (CHead e0 (Bind b) v)))) (\lambda
176 (_: T).(\lambda (e0: C).(drop h d c1 e0)))))))).(let H11 \def (f_equal C C
177 (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _)
178 \Rightarrow c0 | (CHead c2 _ _) \Rightarrow c2])) (CHead c0 k t) (CHead x0
179 (Flat f) t0) (drop_gen_refl (CHead c0 k t) (CHead x0 (Flat f) t0) H10)) in
180 ((let H12 \def (f_equal C K (\lambda (e0: C).(match e0 in C return (\lambda
181 (_: C).K) with [(CSort _) \Rightarrow k | (CHead _ k1 _) \Rightarrow k1]))
182 (CHead c0 k t) (CHead x0 (Flat f) t0) (drop_gen_refl (CHead c0 k t) (CHead x0
183 (Flat f) t0) H10)) in ((let H13 \def (f_equal C T (\lambda (e0: C).(match e0
184 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow t | (CHead _ _ t1)
185 \Rightarrow t1])) (CHead c0 k t) (CHead x0 (Flat f) t0) (drop_gen_refl (CHead
186 c0 k t) (CHead x0 (Flat f) t0) H10)) in (\lambda (H14: (eq K k (Flat
187 f))).(\lambda (H15: (eq C c0 x0)).(let H16 \def (eq_ind_r C x0 (\lambda (c2:
188 C).(clear c2 (CHead c1 (Bind b) u))) (clear_gen_flat f x0 (CHead c1 (Bind b)
189 u) t0 H8) c0 H15) in (let H17 \def (eq_ind_r C x0 (\lambda (c2: C).((drop O O
190 (CHead c0 k t) c2) \to ((clear c2 (CHead c1 (Bind b) u)) \to (ex3_2 T C
191 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
192 T).(\lambda (e0: C).(getl O e (CHead e0 (Bind b) v)))) (\lambda (_:
193 T).(\lambda (e0: C).(drop h d c1 e0))))))) IHx0 c0 H15) in (let H18 \def
194 (eq_ind K k (\lambda (k1: K).((drop O O (CHead c0 k1 t) c0) \to ((clear c0
195 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
196 (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl O e (CHead e0 (Bind b)
197 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) H17 (Flat f)
198 H14) in (let H19 \def (eq_ind K k (\lambda (k1: K).(drop h (S (plus O d))
199 (CHead c0 k1 t) e)) H9 (Flat f) H14) in (ex3_2_ind C T (\lambda (e0:
200 C).(\lambda (v: T).(eq C e (CHead e0 (Flat f) v)))) (\lambda (_: C).(\lambda
201 (v: T).(eq T t (lift h (r (Flat f) (plus O d)) v)))) (\lambda (e0:
202 C).(\lambda (_: T).(drop h (r (Flat f) (plus O d)) c0 e0))) (ex3_2 T C
203 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
204 T).(\lambda (e0: C).(getl O e (CHead e0 (Bind b) v)))) (\lambda (_:
205 T).(\lambda (e0: C).(drop h d c1 e0)))) (\lambda (x1: C).(\lambda (x2:
206 T).(\lambda (H20: (eq C e (CHead x1 (Flat f) x2))).(\lambda (H21: (eq T t
207 (lift h (r (Flat f) (plus O d)) x2))).(\lambda (H22: (drop h (r (Flat f)
208 (plus O d)) c0 x1)).(let H23 \def (f_equal T T (\lambda (e0: T).e0) t (lift h
209 (r (Flat f) (plus O d)) x2) H21) in (let H24 \def (eq_ind C e (\lambda (c2:
210 C).((drop O O (CHead c0 (Flat f) t) c0) \to ((clear c0 (CHead c1 (Bind b) u))
211 \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
212 (\lambda (v: T).(\lambda (e0: C).(getl O c2 (CHead e0 (Bind b) v)))) (\lambda
213 (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) H18 (CHead x1 (Flat f) x2)
214 H20) in (eq_ind_r C (CHead x1 (Flat f) x2) (\lambda (c2: C).(ex3_2 T C
215 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
216 T).(\lambda (e0: C).(getl O c2 (CHead e0 (Bind b) v)))) (\lambda (_:
217 T).(\lambda (e0: C).(drop h d c1 e0))))) (let H25 \def (eq_ind T t (\lambda
218 (t1: T).((drop O O (CHead c0 (Flat f) t1) c0) \to ((clear c0 (CHead c1 (Bind
219 b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
220 (\lambda (v: T).(\lambda (e0: C).(getl O (CHead x1 (Flat f) x2) (CHead e0
221 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) H24
222 (lift h (S d) x2) H23) in (let H26 \def (H c1 u O (getl_intro O c0 (CHead c1
223 (Bind b) u) c0 (drop_refl c0) H16) x1 h d H22) in (ex3_2_ind T C (\lambda (v:
224 T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0:
225 C).(getl O x1 (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop
226 h d c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d
227 v)))) (\lambda (v: T).(\lambda (e0: C).(getl O (CHead x1 (Flat f) x2) (CHead
228 e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))
229 (\lambda (x3: T).(\lambda (x4: C).(\lambda (H27: (eq T u (lift h d
230 x3))).(\lambda (H28: (getl O x1 (CHead x4 (Bind b) x3))).(\lambda (H29: (drop
231 h d c1 x4)).(let H30 \def (eq_ind T u (\lambda (t1: T).((drop O O (CHead c0
232 (Flat f) (lift h (S d) x2)) c0) \to ((clear c0 (CHead c1 (Bind b) t1)) \to
233 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T t1 (lift h d v)))) (\lambda
234 (v: T).(\lambda (e0: C).(getl O (CHead x1 (Flat f) x2) (CHead e0 (Bind b)
235 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) H25 (lift h d
236 x3) H27) in (let H31 \def (eq_ind T u (\lambda (t1: T).(clear c0 (CHead c1
237 (Bind b) t1))) H16 (lift h d x3) H27) in (eq_ind_r T (lift h d x3) (\lambda
238 (t1: T).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T t1 (lift h d v))))
239 (\lambda (v: T).(\lambda (e0: C).(getl O (CHead x1 (Flat f) x2) (CHead e0
240 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0)))))
241 (ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T (lift h d x3) (lift h
242 d v)))) (\lambda (v: T).(\lambda (e0: C).(getl O (CHead x1 (Flat f) x2)
243 (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0)))
244 x3 x4 (refl_equal T (lift h d x3)) (getl_flat x1 (CHead x4 (Bind b) x3) O H28
245 f x2) H29) u H27)))))))) H26))) e H20)))))))) (drop_gen_skip_l c0 e t h (plus
246 O d) (Flat f) H19))))))))) H12)) H11))))) (\lambda (i0: nat).(\lambda (IHi:
247 (((drop h (S (plus i0 d)) (CHead c0 k t) e) \to ((drop i0 O (CHead c0 k t)
248 (CHead x0 (Flat f) t0)) \to ((((drop i0 O (CHead c0 k t) x0) \to ((clear x0
249 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u
250 (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl i0 e (CHead e0 (Bind
251 b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) \to (ex3_2 T
252 C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
253 T).(\lambda (e0: C).(getl i0 e (CHead e0 (Bind b) v)))) (\lambda (_:
254 T).(\lambda (e0: C).(drop h d c1 e0))))))))).(\lambda (H9: (drop h (S (plus
255 (S i0) d)) (CHead c0 k t) e)).(\lambda (H10: (drop (S i0) O (CHead c0 k t)
256 (CHead x0 (Flat f) t0))).(\lambda (IHx0: (((drop (S i0) O (CHead c0 k t) x0)
257 \to ((clear x0 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda
258 (_: C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl (S i0)
259 e (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1
260 e0)))))))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0
261 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r k (plus (S i0) d))
262 v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k (plus (S i0) d)) c0 e0)))
263 (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda
264 (v: T).(\lambda (e0: C).(getl (S i0) e (CHead e0 (Bind b) v)))) (\lambda (_:
265 T).(\lambda (e0: C).(drop h d c1 e0)))) (\lambda (x1: C).(\lambda (x2:
266 T).(\lambda (H11: (eq C e (CHead x1 k x2))).(\lambda (H12: (eq T t (lift h (r
267 k (plus (S i0) d)) x2))).(\lambda (H13: (drop h (r k (plus (S i0) d)) c0
268 x1)).(let H14 \def (f_equal T T (\lambda (e0: T).e0) t (lift h (r k (plus (S
269 i0) d)) x2) H12) in (let H15 \def (eq_ind C e (\lambda (c2: C).((drop h (S
270 (plus i0 d)) (CHead c0 k t) c2) \to ((drop i0 O (CHead c0 k t) (CHead x0
271 (Flat f) t0)) \to ((((drop i0 O (CHead c0 k t) x0) \to ((clear x0 (CHead c1
272 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d
273 v)))) (\lambda (v: T).(\lambda (e0: C).(getl i0 c2 (CHead e0 (Bind b) v))))
274 (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) \to (ex3_2 T C
275 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
276 T).(\lambda (e0: C).(getl i0 c2 (CHead e0 (Bind b) v)))) (\lambda (_:
277 T).(\lambda (e0: C).(drop h d c1 e0)))))))) IHi (CHead x1 k x2) H11) in (let
278 H16 \def (eq_ind C e (\lambda (c2: C).((drop (S i0) O (CHead c0 k t) x0) \to
279 ((clear x0 (CHead c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_:
280 C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl (S i0) c2
281 (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1
282 e0))))))) IHx0 (CHead x1 k x2) H11) in (eq_ind_r C (CHead x1 k x2) (\lambda
283 (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v))))
284 (\lambda (v: T).(\lambda (e0: C).(getl (S i0) c2 (CHead e0 (Bind b) v))))
285 (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))) (let H17 \def (eq_ind T
286 t (\lambda (t1: T).((drop (S i0) O (CHead c0 k t1) x0) \to ((clear x0 (CHead
287 c1 (Bind b) u)) \to (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift
288 h d v)))) (\lambda (v: T).(\lambda (e0: C).(getl (S i0) (CHead x1 k x2)
289 (CHead e0 (Bind b) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1
290 e0))))))) H16 (lift h (r k (S (plus i0 d))) x2) H14) in (let H18 \def (eq_ind
291 T t (\lambda (t1: T).((drop h (S (plus i0 d)) (CHead c0 k t1) (CHead x1 k
292 x2)) \to ((drop i0 O (CHead c0 k t1) (CHead x0 (Flat f) t0)) \to ((((drop i0
293 O (CHead c0 k t1) x0) \to ((clear x0 (CHead c1 (Bind b) u)) \to (ex3_2 T C
294 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
295 T).(\lambda (e0: C).(getl i0 (CHead x1 k x2) (CHead e0 (Bind b) v))))
296 (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) \to (ex3_2 T C
297 (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v:
298 T).(\lambda (e0: C).(getl i0 (CHead x1 k x2) (CHead e0 (Bind b) v))))
299 (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0)))))))) H15 (lift h (r k (S
300 (plus i0 d))) x2) H14) in (let H19 \def (eq_ind nat (r k (plus (S i0) d))
301 (\lambda (n: nat).(drop h n c0 x1)) H13 (plus (r k (S i0)) d) (r_plus k (S
302 i0) d)) in (let H20 \def (eq_ind nat (r k (S i0)) (\lambda (n: nat).(drop h
303 (plus n d) c0 x1)) H19 (S (r k i0)) (r_S k i0)) in (let H21 \def (H c1 u (r k
304 i0) (getl_intro (r k i0) c0 (CHead c1 (Bind b) u) (CHead x0 (Flat f) t0)
305 (drop_gen_drop k c0 (CHead x0 (Flat f) t0) t i0 H10) (clear_flat x0 (CHead c1
306 (Bind b) u) (clear_gen_flat f x0 (CHead c1 (Bind b) u) t0 H8) f t0)) x1 h d
307 H20) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h d
308 v)))) (\lambda (v: T).(\lambda (e0: C).(getl (r k i0) x1 (CHead e0 (Bind b)
309 v)))) (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))) (ex3_2 T C (\lambda
310 (v: T).(\lambda (_: C).(eq T u (lift h d v)))) (\lambda (v: T).(\lambda (e0:
311 C).(getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)))) (\lambda (_:
312 T).(\lambda (e0: C).(drop h d c1 e0)))) (\lambda (x3: T).(\lambda (x4:
313 C).(\lambda (H22: (eq T u (lift h d x3))).(\lambda (H23: (getl (r k i0) x1
314 (CHead x4 (Bind b) x3))).(\lambda (H24: (drop h d c1 x4)).(let H25 \def
315 (eq_ind T u (\lambda (t1: T).((drop (S i0) O (CHead c0 k (lift h (r k (S
316 (plus i0 d))) x2)) x0) \to ((clear x0 (CHead c1 (Bind b) t1)) \to (ex3_2 T C
317 (\lambda (v: T).(\lambda (_: C).(eq T t1 (lift h d v)))) (\lambda (v:
318 T).(\lambda (e0: C).(getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v))))
319 (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))))))) H17 (lift h d x3)
320 H22) in (let H26 \def (eq_ind T u (\lambda (t1: T).(clear x0 (CHead c1 (Bind
321 b) t1))) (clear_gen_flat f x0 (CHead c1 (Bind b) u) t0 H8) (lift h d x3) H22)
322 in (eq_ind_r T (lift h d x3) (\lambda (t1: T).(ex3_2 T C (\lambda (v:
323 T).(\lambda (_: C).(eq T t1 (lift h d v)))) (\lambda (v: T).(\lambda (e0:
324 C).(getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v)))) (\lambda (_:
325 T).(\lambda (e0: C).(drop h d c1 e0))))) (ex3_2_intro T C (\lambda (v:
326 T).(\lambda (_: C).(eq T (lift h d x3) (lift h d v)))) (\lambda (v:
327 T).(\lambda (e0: C).(getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v))))
328 (\lambda (_: T).(\lambda (e0: C).(drop h d c1 e0))) x3 x4 (refl_equal T (lift
329 h d x3)) (getl_head k i0 x1 (CHead x4 (Bind b) x3) H23 x2) H24) u H22))))))))
330 H21)))))) e H11))))))))) (drop_gen_skip_l c0 e t h (plus (S i0) d) k
331 H9))))))) i H1 H7 IHx)))) k0 H5 H6))))))) x H3 H4)))) H2)))))))))))))) c)).
333 theorem getl_drop_conf_ge:
334 \forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall
335 (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c e) \to ((le (plus d
336 h) i) \to (getl (minus i h) e a)))))))))
338 \lambda (i: nat).(\lambda (a: C).(\lambda (c: C).(\lambda (H: (getl i c
339 a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H0: (drop h
340 d c e)).(\lambda (H1: (le (plus d h) i)).(let H2 \def (getl_gen_all c a i H)
341 in (ex2_ind C (\lambda (e0: C).(drop i O c e0)) (\lambda (e0: C).(clear e0
342 a)) (getl (minus i h) e a) (\lambda (x: C).(\lambda (H3: (drop i O c
343 x)).(\lambda (H4: (clear x a)).(getl_intro (minus i h) e a x (drop_conf_ge i
344 x c H3 e h d H0 H1) H4)))) H2)))))))))).
346 theorem getl_conf_ge_drop:
347 \forall (b: B).(\forall (c1: C).(\forall (e: C).(\forall (u: T).(\forall (i:
348 nat).((getl i c1 (CHead e (Bind b) u)) \to (\forall (c2: C).((drop (S O) i c1
349 c2) \to (drop i O c2 e))))))))
351 \lambda (b: B).(\lambda (c1: C).(\lambda (e: C).(\lambda (u: T).(\lambda (i:
352 nat).(\lambda (H: (getl i c1 (CHead e (Bind b) u))).(\lambda (c2: C).(\lambda
353 (H0: (drop (S O) i c1 c2)).(let H3 \def (eq_ind nat (minus (S i) (S O))
354 (\lambda (n: nat).(drop n O c2 e)) (drop_conf_ge (S i) e c1 (getl_drop b c1 e
355 u i H) c2 (S O) i H0 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(le n (S
356 i))) (le_n (S i)) (plus i (S O)) (plus_sym i (S O)))) i (minus_Sx_SO i)) in
359 theorem getl_drop_conf_rev:
360 \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to
361 (\forall (b: B).(\forall (c2: C).(\forall (v2: T).(\forall (i: nat).((getl i
362 c2 (CHead e2 (Bind b) v2)) \to (ex2 C (\lambda (c1: C).(drop j O c1 c2))
363 (\lambda (c1: C).(drop (S i) j c1 e1)))))))))))
365 \lambda (j: nat).(\lambda (e1: C).(\lambda (e2: C).(\lambda (H: (drop j O e1
366 e2)).(\lambda (b: B).(\lambda (c2: C).(\lambda (v2: T).(\lambda (i:
367 nat).(\lambda (H0: (getl i c2 (CHead e2 (Bind b) v2))).(drop_conf_rev j e1 e2
368 H c2 (S i) (getl_drop b c2 e2 v2 i H0)))))))))).
370 theorem drop_getl_trans_lt:
371 \forall (i: nat).(\forall (d: nat).((lt i d) \to (\forall (c1: C).(\forall
372 (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (b: B).(\forall (e2:
373 C).(\forall (v: T).((getl i c2 (CHead e2 (Bind b) v)) \to (ex2 C (\lambda
374 (e1: C).(getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v)))) (\lambda
375 (e1: C).(drop h (minus d (S i)) e1 e2)))))))))))))
377 \lambda (i: nat).(\lambda (d: nat).(\lambda (H: (lt i d)).(\lambda (c1:
378 C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (H0: (drop h d c1
379 c2)).(\lambda (b: B).(\lambda (e2: C).(\lambda (v: T).(\lambda (H1: (getl i
380 c2 (CHead e2 (Bind b) v))).(let H2 \def (getl_gen_all c2 (CHead e2 (Bind b)
381 v) i H1) in (ex2_ind C (\lambda (e: C).(drop i O c2 e)) (\lambda (e:
382 C).(clear e (CHead e2 (Bind b) v))) (ex2 C (\lambda (e1: C).(getl i c1 (CHead
383 e1 (Bind b) (lift h (minus d (S i)) v)))) (\lambda (e1: C).(drop h (minus d
384 (S i)) e1 e2))) (\lambda (x: C).(\lambda (H3: (drop i O c2 x)).(\lambda (H4:
385 (clear x (CHead e2 (Bind b) v))).(ex2_ind C (\lambda (e1: C).(drop i O c1
386 e1)) (\lambda (e1: C).(drop h (minus d i) e1 x)) (ex2 C (\lambda (e1:
387 C).(getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v)))) (\lambda (e1:
388 C).(drop h (minus d (S i)) e1 e2))) (\lambda (x0: C).(\lambda (H5: (drop i O
389 c1 x0)).(\lambda (H6: (drop h (minus d i) x0 x)).(let H7 \def (eq_ind nat
390 (minus d i) (\lambda (n: nat).(drop h n x0 x)) H6 (S (minus d (S i)))
391 (minus_x_Sy d i H)) in (let H8 \def (drop_clear_S x x0 h (minus d (S i)) H7 b
392 e2 v H4) in (ex2_ind C (\lambda (c3: C).(clear x0 (CHead c3 (Bind b) (lift h
393 (minus d (S i)) v)))) (\lambda (c3: C).(drop h (minus d (S i)) c3 e2)) (ex2 C
394 (\lambda (e1: C).(getl i c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v))))
395 (\lambda (e1: C).(drop h (minus d (S i)) e1 e2))) (\lambda (x1: C).(\lambda
396 (H9: (clear x0 (CHead x1 (Bind b) (lift h (minus d (S i)) v)))).(\lambda
397 (H10: (drop h (minus d (S i)) x1 e2)).(ex_intro2 C (\lambda (e1: C).(getl i
398 c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v)))) (\lambda (e1: C).(drop h
399 (minus d (S i)) e1 e2)) x1 (getl_intro i c1 (CHead x1 (Bind b) (lift h (minus
400 d (S i)) v)) x0 H5 H9) H10)))) H8)))))) (drop_trans_le i d (le_S_n i d (le_S
401 (S i) d H)) c1 c2 h H0 x H3))))) H2)))))))))))).
403 theorem drop_getl_trans_le:
404 \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall
405 (c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((getl i c2
406 e2) \to (ex3_2 C C (\lambda (e0: C).(\lambda (_: C).(drop i O c1 e0)))
407 (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d i) e0 e1))) (\lambda (_:
408 C).(\lambda (e1: C).(clear e1 e2))))))))))))
410 \lambda (i: nat).(\lambda (d: nat).(\lambda (H: (le i d)).(\lambda (c1:
411 C).(\lambda (c2: C).(\lambda (h: nat).(\lambda (H0: (drop h d c1
412 c2)).(\lambda (e2: C).(\lambda (H1: (getl i c2 e2)).(let H2 \def
413 (getl_gen_all c2 e2 i H1) in (ex2_ind C (\lambda (e: C).(drop i O c2 e))
414 (\lambda (e: C).(clear e e2)) (ex3_2 C C (\lambda (e0: C).(\lambda (_:
415 C).(drop i O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d i)
416 e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 e2)))) (\lambda (x:
417 C).(\lambda (H3: (drop i O c2 x)).(\lambda (H4: (clear x e2)).(let H5 \def
418 (drop_trans_le i d H c1 c2 h H0 x H3) in (ex2_ind C (\lambda (e1: C).(drop i
419 O c1 e1)) (\lambda (e1: C).(drop h (minus d i) e1 x)) (ex3_2 C C (\lambda
420 (e0: C).(\lambda (_: C).(drop i O c1 e0))) (\lambda (e0: C).(\lambda (e1:
421 C).(drop h (minus d i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
422 e2)))) (\lambda (x0: C).(\lambda (H6: (drop i O c1 x0)).(\lambda (H7: (drop h
423 (minus d i) x0 x)).(ex3_2_intro C C (\lambda (e0: C).(\lambda (_: C).(drop i
424 O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d i) e0 e1)))
425 (\lambda (_: C).(\lambda (e1: C).(clear e1 e2))) x0 x H6 H7 H4)))) H5)))))
428 theorem drop_getl_trans_ge:
429 \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d:
430 nat).(\forall (h: nat).((drop h d c1 c2) \to (\forall (e2: C).((getl i c2 e2)
431 \to ((le d i) \to (getl (plus i h) c1 e2)))))))))
433 \lambda (i: nat).(\lambda (c1: C).(\lambda (c2: C).(\lambda (d:
434 nat).(\lambda (h: nat).(\lambda (H: (drop h d c1 c2)).(\lambda (e2:
435 C).(\lambda (H0: (getl i c2 e2)).(\lambda (H1: (le d i)).(let H2 \def
436 (getl_gen_all c2 e2 i H0) in (ex2_ind C (\lambda (e: C).(drop i O c2 e))
437 (\lambda (e: C).(clear e e2)) (getl (plus i h) c1 e2) (\lambda (x:
438 C).(\lambda (H3: (drop i O c2 x)).(\lambda (H4: (clear x e2)).(getl_intro
439 (plus i h) c1 e2 x (drop_trans_ge i c1 c2 d h H x H3 H1) H4)))) H2)))))))))).
441 theorem getl_drop_trans:
442 \forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl h c1 c2) \to
443 (\forall (e2: C).(\forall (i: nat).((drop (S i) O c2 e2) \to (drop (S (plus i
446 \lambda (c1: C).(C_ind (\lambda (c: C).(\forall (c2: C).(\forall (h:
447 nat).((getl h c c2) \to (\forall (e2: C).(\forall (i: nat).((drop (S i) O c2
448 e2) \to (drop (S (plus i h)) O c e2)))))))) (\lambda (n: nat).(\lambda (c2:
449 C).(\lambda (h: nat).(\lambda (H: (getl h (CSort n) c2)).(\lambda (e2:
450 C).(\lambda (i: nat).(\lambda (_: (drop (S i) O c2 e2)).(getl_gen_sort n h c2
451 H (drop (S (plus i h)) O (CSort n) e2))))))))) (\lambda (c2: C).(\lambda
452 (IHc: ((\forall (c3: C).(\forall (h: nat).((getl h c2 c3) \to (\forall (e2:
453 C).(\forall (i: nat).((drop (S i) O c3 e2) \to (drop (S (plus i h)) O c2
454 e2))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(\forall
455 (c3: C).(\forall (h: nat).((getl h (CHead c2 k0 t) c3) \to (\forall (e2:
456 C).(\forall (i: nat).((drop (S i) O c3 e2) \to (drop (S (plus i h)) O (CHead
457 c2 k0 t) e2))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (c3:
458 C).(\lambda (h: nat).(nat_ind (\lambda (n: nat).((getl n (CHead c2 (Bind b)
459 t) c3) \to (\forall (e2: C).(\forall (i: nat).((drop (S i) O c3 e2) \to (drop
460 (S (plus i n)) O (CHead c2 (Bind b) t) e2)))))) (\lambda (H: (getl O (CHead
461 c2 (Bind b) t) c3)).(\lambda (e2: C).(\lambda (i: nat).(\lambda (H0: (drop (S
462 i) O c3 e2)).(let H1 \def (eq_ind C c3 (\lambda (c: C).(drop (S i) O c e2))
463 H0 (CHead c2 (Bind b) t) (clear_gen_bind b c2 c3 t (getl_gen_O (CHead c2
464 (Bind b) t) c3 H))) in (eq_ind nat i (\lambda (n: nat).(drop (S n) O (CHead
465 c2 (Bind b) t) e2)) (drop_drop (Bind b) i c2 e2 (drop_gen_drop (Bind b) c2 e2
466 t i H1) t) (plus i O) (plus_n_O i))))))) (\lambda (n: nat).(\lambda (_:
467 (((getl n (CHead c2 (Bind b) t) c3) \to (\forall (e2: C).(\forall (i:
468 nat).((drop (S i) O c3 e2) \to (drop (S (plus i n)) O (CHead c2 (Bind b) t)
469 e2))))))).(\lambda (H0: (getl (S n) (CHead c2 (Bind b) t) c3)).(\lambda (e2:
470 C).(\lambda (i: nat).(\lambda (H1: (drop (S i) O c3 e2)).(eq_ind nat (plus (S
471 i) n) (\lambda (n0: nat).(drop (S n0) O (CHead c2 (Bind b) t) e2)) (drop_drop
472 (Bind b) (plus (S i) n) c2 e2 (IHc c3 n (getl_gen_S (Bind b) c2 c3 t n H0) e2
473 i H1) t) (plus i (S n)) (plus_Snm_nSm i n)))))))) h))))) (\lambda (f:
474 F).(\lambda (t: T).(\lambda (c3: C).(\lambda (h: nat).(nat_ind (\lambda (n:
475 nat).((getl n (CHead c2 (Flat f) t) c3) \to (\forall (e2: C).(\forall (i:
476 nat).((drop (S i) O c3 e2) \to (drop (S (plus i n)) O (CHead c2 (Flat f) t)
477 e2)))))) (\lambda (H: (getl O (CHead c2 (Flat f) t) c3)).(\lambda (e2:
478 C).(\lambda (i: nat).(\lambda (H0: (drop (S i) O c3 e2)).(drop_drop (Flat f)
479 (plus i O) c2 e2 (IHc c3 O (getl_intro O c2 c3 c2 (drop_refl c2)
480 (clear_gen_flat f c2 c3 t (getl_gen_O (CHead c2 (Flat f) t) c3 H))) e2 i H0)
481 t))))) (\lambda (n: nat).(\lambda (_: (((getl n (CHead c2 (Flat f) t) c3) \to
482 (\forall (e2: C).(\forall (i: nat).((drop (S i) O c3 e2) \to (drop (S (plus i
483 n)) O (CHead c2 (Flat f) t) e2))))))).(\lambda (H0: (getl (S n) (CHead c2
484 (Flat f) t) c3)).(\lambda (e2: C).(\lambda (i: nat).(\lambda (H1: (drop (S i)
485 O c3 e2)).(drop_drop (Flat f) (plus i (S n)) c2 e2 (IHc c3 (S n) (getl_gen_S
486 (Flat f) c2 c3 t n H0) e2 i H1) t))))))) h))))) k)))) c1).
projects / helm.git / blob