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