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/LambdaDelta-1/drop/fwd".
19 include "drop/defs.ma".
21 theorem drop_gen_sort:
22 \forall (n: nat).(\forall (h: nat).(\forall (d: nat).(\forall (x: C).((drop
23 h d (CSort n) x) \to (and3 (eq C x (CSort n)) (eq nat h O) (eq nat d O))))))
25 \lambda (n: nat).(\lambda (h: nat).(\lambda (d: nat).(\lambda (x:
26 C).(\lambda (H: (drop h d (CSort n) x)).(insert_eq C (CSort n) (\lambda (c:
27 C).(drop h d c x)) (\lambda (c: C).(and3 (eq C x c) (eq nat h O) (eq nat d
28 O))) (\lambda (y: C).(\lambda (H0: (drop h d y x)).(drop_ind (\lambda (n0:
29 nat).(\lambda (n1: nat).(\lambda (c: C).(\lambda (c0: C).((eq C c (CSort n))
30 \to (and3 (eq C c0 c) (eq nat n0 O) (eq nat n1 O))))))) (\lambda (c:
31 C).(\lambda (H1: (eq C c (CSort n))).(let H2 \def (f_equal C C (\lambda (e:
32 C).e) c (CSort n) H1) in (eq_ind_r C (CSort n) (\lambda (c0: C).(and3 (eq C
33 c0 c0) (eq nat O O) (eq nat O O))) (and3_intro (eq C (CSort n) (CSort n)) (eq
34 nat O O) (eq nat O O) (refl_equal C (CSort n)) (refl_equal nat O) (refl_equal
35 nat O)) c H2)))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (c: C).(\lambda
36 (e: C).(\lambda (_: (drop (r k h0) O c e)).(\lambda (_: (((eq C c (CSort n))
37 \to (and3 (eq C e c) (eq nat (r k h0) O) (eq nat O O))))).(\lambda (u:
38 T).(\lambda (H3: (eq C (CHead c k u) (CSort n))).(let H4 \def (eq_ind C
39 (CHead c k u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop)
40 with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
41 (CSort n) H3) in (False_ind (and3 (eq C e (CHead c k u)) (eq nat (S h0) O)
42 (eq nat O O)) H4)))))))))) (\lambda (k: K).(\lambda (h0: nat).(\lambda (d0:
43 nat).(\lambda (c: C).(\lambda (e: C).(\lambda (_: (drop h0 (r k d0) c
44 e)).(\lambda (_: (((eq C c (CSort n)) \to (and3 (eq C e c) (eq nat h0 O) (eq
45 nat (r k d0) O))))).(\lambda (u: T).(\lambda (H3: (eq C (CHead c k (lift h0
46 (r k d0) u)) (CSort n))).(let H4 \def (eq_ind C (CHead c k (lift h0 (r k d0)
47 u)) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort
48 _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort n) H3) in
49 (False_ind (and3 (eq C (CHead e k u) (CHead c k (lift h0 (r k d0) u))) (eq
50 nat h0 O) (eq nat (S d0) O)) H4))))))))))) h d y x H0))) H))))).
52 theorem drop_gen_refl:
53 \forall (x: C).(\forall (e: C).((drop O O x e) \to (eq C x e)))
55 \lambda (x: C).(\lambda (e: C).(\lambda (H: (drop O O x e)).(insert_eq nat O
56 (\lambda (n: nat).(drop n O x e)) (\lambda (_: nat).(eq C x e)) (\lambda (y:
57 nat).(\lambda (H0: (drop y O x e)).(insert_eq nat O (\lambda (n: nat).(drop y
58 n x e)) (\lambda (n: nat).((eq nat y n) \to (eq C x e))) (\lambda (y0:
59 nat).(\lambda (H1: (drop y y0 x e)).(drop_ind (\lambda (n: nat).(\lambda (n0:
60 nat).(\lambda (c: C).(\lambda (c0: C).((eq nat n0 O) \to ((eq nat n n0) \to
61 (eq C c c0))))))) (\lambda (c: C).(\lambda (_: (eq nat O O)).(\lambda (_: (eq
62 nat O O)).(refl_equal C c)))) (\lambda (k: K).(\lambda (h: nat).(\lambda (c:
63 C).(\lambda (e0: C).(\lambda (_: (drop (r k h) O c e0)).(\lambda (_: (((eq
64 nat O O) \to ((eq nat (r k h) O) \to (eq C c e0))))).(\lambda (u: T).(\lambda
65 (_: (eq nat O O)).(\lambda (H5: (eq nat (S h) O)).(let H6 \def (eq_ind nat (S
66 h) (\lambda (ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O
67 \Rightarrow False | (S _) \Rightarrow True])) I O H5) in (False_ind (eq C
68 (CHead c k u) e0) H6))))))))))) (\lambda (k: K).(\lambda (h: nat).(\lambda
69 (d: nat).(\lambda (c: C).(\lambda (e0: C).(\lambda (H2: (drop h (r k d) c
70 e0)).(\lambda (H3: (((eq nat (r k d) O) \to ((eq nat h (r k d)) \to (eq C c
71 e0))))).(\lambda (u: T).(\lambda (H4: (eq nat (S d) O)).(\lambda (H5: (eq nat
72 h (S d))).(let H6 \def (f_equal nat nat (\lambda (e1: nat).e1) h (S d) H5) in
73 (let H7 \def (eq_ind nat h (\lambda (n: nat).((eq nat (r k d) O) \to ((eq nat
74 n (r k d)) \to (eq C c e0)))) H3 (S d) H6) in (let H8 \def (eq_ind nat h
75 (\lambda (n: nat).(drop n (r k d) c e0)) H2 (S d) H6) in (eq_ind_r nat (S d)
76 (\lambda (n: nat).(eq C (CHead c k (lift n (r k d) u)) (CHead e0 k u))) (let
77 H9 \def (eq_ind nat (S d) (\lambda (ee: nat).(match ee in nat return (\lambda
78 (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H4)
79 in (False_ind (eq C (CHead c k (lift (S d) (r k d) u)) (CHead e0 k u)) H9)) h
80 H6)))))))))))))) y y0 x e H1))) H0))) H))).
82 theorem drop_gen_drop:
83 \forall (k: K).(\forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h:
84 nat).((drop (S h) O (CHead c k u) x) \to (drop (r k h) O c x))))))
86 \lambda (k: K).(\lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h:
87 nat).(\lambda (H: (drop (S h) O (CHead c k u) x)).(insert_eq C (CHead c k u)
88 (\lambda (c0: C).(drop (S h) O c0 x)) (\lambda (_: C).(drop (r k h) O c x))
89 (\lambda (y: C).(\lambda (H0: (drop (S h) O y x)).(insert_eq nat O (\lambda
90 (n: nat).(drop (S h) n y x)) (\lambda (n: nat).((eq C y (CHead c k u)) \to
91 (drop (r k h) n c x))) (\lambda (y0: nat).(\lambda (H1: (drop (S h) y0 y
92 x)).(insert_eq nat (S h) (\lambda (n: nat).(drop n y0 y x)) (\lambda (_:
93 nat).((eq nat y0 O) \to ((eq C y (CHead c k u)) \to (drop (r k h) y0 c x))))
94 (\lambda (y1: nat).(\lambda (H2: (drop y1 y0 y x)).(drop_ind (\lambda (n:
95 nat).(\lambda (n0: nat).(\lambda (c0: C).(\lambda (c1: C).((eq nat n (S h))
96 \to ((eq nat n0 O) \to ((eq C c0 (CHead c k u)) \to (drop (r k h) n0 c
97 c1)))))))) (\lambda (c0: C).(\lambda (H3: (eq nat O (S h))).(\lambda (_: (eq
98 nat O O)).(\lambda (_: (eq C c0 (CHead c k u))).(let H6 \def (match H3 in eq
99 return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n (S h)) \to (drop
100 (r k h) O c c0)))) with [refl_equal \Rightarrow (\lambda (H6: (eq nat O (S
101 h))).(let H7 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return
102 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
103 I (S h) H6) in (False_ind (drop (r k h) O c c0) H7)))]) in (H6 (refl_equal
104 nat (S h)))))))) (\lambda (k0: K).(\lambda (h0: nat).(\lambda (c0:
105 C).(\lambda (e: C).(\lambda (H3: (drop (r k0 h0) O c0 e)).(\lambda (_: (((eq
106 nat (r k0 h0) (S h)) \to ((eq nat O O) \to ((eq C c0 (CHead c k u)) \to (drop
107 (r k h) O c e)))))).(\lambda (u0: T).(\lambda (H5: (eq nat (S h0) (S
108 h))).(\lambda (_: (eq nat O O)).(\lambda (H7: (eq C (CHead c0 k0 u0) (CHead c
109 k u))).(let H8 \def (match H5 in eq return (\lambda (n: nat).(\lambda (_: (eq
110 ? ? n)).((eq nat n (S h)) \to (drop (r k h) O c e)))) with [refl_equal
111 \Rightarrow (\lambda (H8: (eq nat (S h0) (S h))).(let H9 \def (f_equal nat
112 nat (\lambda (e0: nat).(match e0 in nat return (\lambda (_: nat).nat) with [O
113 \Rightarrow h0 | (S n) \Rightarrow n])) (S h0) (S h) H8) in (eq_ind nat h
114 (\lambda (_: nat).(drop (r k h) O c e)) (let H10 \def (match H7 in eq return
115 (\lambda (c1: C).(\lambda (_: (eq ? ? c1)).((eq C c1 (CHead c k u)) \to (drop
116 (r k h) O c e)))) with [refl_equal \Rightarrow (\lambda (H10: (eq C (CHead c0
117 k0 u0) (CHead c k u))).(let H11 \def (f_equal C T (\lambda (e0: C).(match e0
118 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t)
119 \Rightarrow t])) (CHead c0 k0 u0) (CHead c k u) H10) in ((let H12 \def
120 (f_equal C K (\lambda (e0: C).(match e0 in C return (\lambda (_: C).K) with
121 [(CSort _) \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead c0 k0 u0)
122 (CHead c k u) H10) in ((let H13 \def (f_equal C C (\lambda (e0: C).(match e0
123 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c1 _
124 _) \Rightarrow c1])) (CHead c0 k0 u0) (CHead c k u) H10) in (eq_ind C c
125 (\lambda (_: C).((eq K k0 k) \to ((eq T u0 u) \to (drop (r k h) O c e))))
126 (\lambda (H14: (eq K k0 k)).(eq_ind K k (\lambda (_: K).((eq T u0 u) \to
127 (drop (r k h) O c e))) (\lambda (H15: (eq T u0 u)).(eq_ind T u (\lambda (_:
128 T).(drop (r k h) O c e)) (eq_ind nat h0 (\lambda (n: nat).(drop (r k n) O c
129 e)) (eq_ind C c0 (\lambda (c1: C).(drop (r k h0) O c1 e)) (eq_ind K k0
130 (\lambda (k1: K).(drop (r k1 h0) O c0 e)) H3 k H14) c H13) h H9) u0 (sym_eq T
131 u0 u H15))) k0 (sym_eq K k0 k H14))) c0 (sym_eq C c0 c H13))) H12)) H11)))])
132 in (H10 (refl_equal C (CHead c k u)))) h0 (sym_eq nat h0 h H9))))]) in (H8
133 (refl_equal nat (S h)))))))))))))) (\lambda (k0: K).(\lambda (h0:
134 nat).(\lambda (d: nat).(\lambda (c0: C).(\lambda (e: C).(\lambda (_: (drop h0
135 (r k0 d) c0 e)).(\lambda (_: (((eq nat h0 (S h)) \to ((eq nat (r k0 d) O) \to
136 ((eq C c0 (CHead c k u)) \to (drop (r k h) (r k0 d) c e)))))).(\lambda (u0:
137 T).(\lambda (_: (eq nat h0 (S h))).(\lambda (H6: (eq nat (S d) O)).(\lambda
138 (_: (eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k u))).(let H8 \def
139 (match H6 in eq return (\lambda (n: nat).(\lambda (_: (eq ? ? n)).((eq nat n
140 O) \to (drop (r k h) (S d) c (CHead e k0 u0))))) with [refl_equal \Rightarrow
141 (\lambda (H8: (eq nat (S d) O)).(let H9 \def (eq_ind nat (S d) (\lambda (e0:
142 nat).(match e0 in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
143 False | (S _) \Rightarrow True])) I O H8) in (False_ind (drop (r k h) (S d) c
144 (CHead e k0 u0)) H9)))]) in (H8 (refl_equal nat O)))))))))))))) y1 y0 y x
145 H2))) H1))) H0))) H)))))).
147 theorem drop_gen_skip_r:
148 \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall
149 (d: nat).(\forall (k: K).((drop h (S d) x (CHead c k u)) \to (ex2 C (\lambda
150 (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e: C).(drop h (r k
153 \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda
154 (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) x (CHead c k u))).(let H0
155 \def (match H in drop return (\lambda (n: nat).(\lambda (n0: nat).(\lambda
156 (c0: C).(\lambda (c1: C).(\lambda (_: (drop n n0 c0 c1)).((eq nat n h) \to
157 ((eq nat n0 (S d)) \to ((eq C c0 x) \to ((eq C c1 (CHead c k u)) \to (ex2 C
158 (\lambda (e: C).(eq C x (CHead e k (lift h (r k d) u)))) (\lambda (e:
159 C).(drop h (r k d) e c)))))))))))) with [(drop_refl c0) \Rightarrow (\lambda
160 (H0: (eq nat O h)).(\lambda (H1: (eq nat O (S d))).(\lambda (H2: (eq C c0
161 x)).(\lambda (H3: (eq C c0 (CHead c k u))).(eq_ind nat O (\lambda (n:
162 nat).((eq nat O (S d)) \to ((eq C c0 x) \to ((eq C c0 (CHead c k u)) \to (ex2
163 C (\lambda (e: C).(eq C x (CHead e k (lift n (r k d) u)))) (\lambda (e:
164 C).(drop n (r k d) e c))))))) (\lambda (H4: (eq nat O (S d))).(let H5 \def
165 (eq_ind nat O (\lambda (e: nat).(match e in nat return (\lambda (_:
166 nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4)
167 in (False_ind ((eq C c0 x) \to ((eq C c0 (CHead c k u)) \to (ex2 C (\lambda
168 (e: C).(eq C x (CHead e k (lift O (r k d) u)))) (\lambda (e: C).(drop O (r k
169 d) e c))))) H5))) h H0 H1 H2 H3))))) | (drop_drop k0 h0 c0 e H0 u0)
170 \Rightarrow (\lambda (H1: (eq nat (S h0) h)).(\lambda (H2: (eq nat O (S
171 d))).(\lambda (H3: (eq C (CHead c0 k0 u0) x)).(\lambda (H4: (eq C e (CHead c
172 k u))).(eq_ind nat (S h0) (\lambda (n: nat).((eq nat O (S d)) \to ((eq C
173 (CHead c0 k0 u0) x) \to ((eq C e (CHead c k u)) \to ((drop (r k0 h0) O c0 e)
174 \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift n (r k d) u))))
175 (\lambda (e0: C).(drop n (r k d) e0 c)))))))) (\lambda (H5: (eq nat O (S
176 d))).(let H6 \def (eq_ind nat O (\lambda (e0: nat).(match e0 in nat return
177 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
178 I (S d) H5) in (False_ind ((eq C (CHead c0 k0 u0) x) \to ((eq C e (CHead c k
179 u)) \to ((drop (r k0 h0) O c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead
180 e0 k (lift (S h0) (r k d) u)))) (\lambda (e0: C).(drop (S h0) (r k d) e0
181 c)))))) H6))) h H1 H2 H3 H4 H0))))) | (drop_skip k0 h0 d0 c0 e H0 u0)
182 \Rightarrow (\lambda (H1: (eq nat h0 h)).(\lambda (H2: (eq nat (S d0) (S
183 d))).(\lambda (H3: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) x)).(\lambda
184 (H4: (eq C (CHead e k0 u0) (CHead c k u))).(eq_ind nat h (\lambda (n:
185 nat).((eq nat (S d0) (S d)) \to ((eq C (CHead c0 k0 (lift n (r k0 d0) u0)) x)
186 \to ((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop n (r k0 d0) c0 e) \to
187 (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift h (r k d) u)))) (\lambda
188 (e0: C).(drop h (r k d) e0 c)))))))) (\lambda (H5: (eq nat (S d0) (S
189 d))).(let H6 \def (f_equal nat nat (\lambda (e0: nat).(match e0 in nat return
190 (\lambda (_: nat).nat) with [O \Rightarrow d0 | (S n) \Rightarrow n])) (S d0)
191 (S d) H5) in (eq_ind nat d (\lambda (n: nat).((eq C (CHead c0 k0 (lift h (r
192 k0 n) u0)) x) \to ((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop h (r k0 n)
193 c0 e) \to (ex2 C (\lambda (e0: C).(eq C x (CHead e0 k (lift h (r k d) u))))
194 (\lambda (e0: C).(drop h (r k d) e0 c))))))) (\lambda (H7: (eq C (CHead c0 k0
195 (lift h (r k0 d) u0)) x)).(eq_ind C (CHead c0 k0 (lift h (r k0 d) u0))
196 (\lambda (c1: C).((eq C (CHead e k0 u0) (CHead c k u)) \to ((drop h (r k0 d)
197 c0 e) \to (ex2 C (\lambda (e0: C).(eq C c1 (CHead e0 k (lift h (r k d) u))))
198 (\lambda (e0: C).(drop h (r k d) e0 c)))))) (\lambda (H8: (eq C (CHead e k0
199 u0) (CHead c k u))).(let H9 \def (f_equal C T (\lambda (e0: C).(match e0 in C
200 return (\lambda (_: C).T) with [(CSort _) \Rightarrow u0 | (CHead _ _ t)
201 \Rightarrow t])) (CHead e k0 u0) (CHead c k u) H8) in ((let H10 \def (f_equal
202 C K (\lambda (e0: C).(match e0 in C return (\lambda (_: C).K) with [(CSort _)
203 \Rightarrow k0 | (CHead _ k1 _) \Rightarrow k1])) (CHead e k0 u0) (CHead c k
204 u) H8) in ((let H11 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
205 (\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c1 _ _) \Rightarrow
206 c1])) (CHead e k0 u0) (CHead c k u) H8) in (eq_ind C c (\lambda (c1: C).((eq
207 K k0 k) \to ((eq T u0 u) \to ((drop h (r k0 d) c0 c1) \to (ex2 C (\lambda
208 (e0: C).(eq C (CHead c0 k0 (lift h (r k0 d) u0)) (CHead e0 k (lift h (r k d)
209 u)))) (\lambda (e0: C).(drop h (r k d) e0 c))))))) (\lambda (H12: (eq K k0
210 k)).(eq_ind K k (\lambda (k1: K).((eq T u0 u) \to ((drop h (r k1 d) c0 c) \to
211 (ex2 C (\lambda (e0: C).(eq C (CHead c0 k1 (lift h (r k1 d) u0)) (CHead e0 k
212 (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c)))))) (\lambda
213 (H13: (eq T u0 u)).(eq_ind T u (\lambda (t: T).((drop h (r k d) c0 c) \to
214 (ex2 C (\lambda (e0: C).(eq C (CHead c0 k (lift h (r k d) t)) (CHead e0 k
215 (lift h (r k d) u)))) (\lambda (e0: C).(drop h (r k d) e0 c))))) (\lambda
216 (H14: (drop h (r k d) c0 c)).(let H15 \def (eq_ind T u0 (\lambda (t: T).(eq C
217 (CHead c0 k0 (lift h (r k0 d) t)) x)) H7 u H13) in (let H16 \def (eq_ind K k0
218 (\lambda (k1: K).(eq C (CHead c0 k1 (lift h (r k1 d) u)) x)) H15 k H12) in
219 (let H17 \def (eq_ind_r C x (\lambda (c1: C).(drop h (S d) c1 (CHead c k u)))
220 H (CHead c0 k (lift h (r k d) u)) H16) in (ex_intro2 C (\lambda (e0: C).(eq C
221 (CHead c0 k (lift h (r k d) u)) (CHead e0 k (lift h (r k d) u)))) (\lambda
222 (e0: C).(drop h (r k d) e0 c)) c0 (refl_equal C (CHead c0 k (lift h (r k d)
223 u))) H14))))) u0 (sym_eq T u0 u H13))) k0 (sym_eq K k0 k H12))) e (sym_eq C e
224 c H11))) H10)) H9))) x H7)) d0 (sym_eq nat d0 d H6)))) h0 (sym_eq nat h0 h
225 H1) H2 H3 H4 H0)))))]) in (H0 (refl_equal nat h) (refl_equal nat (S d))
226 (refl_equal C x) (refl_equal C (CHead c k u)))))))))).
228 theorem drop_gen_skip_l:
229 \forall (c: C).(\forall (x: C).(\forall (u: T).(\forall (h: nat).(\forall
230 (d: nat).(\forall (k: K).((drop h (S d) (CHead c k u) x) \to (ex3_2 C T
231 (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_:
232 C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_:
233 T).(drop h (r k d) c e))))))))))
235 \lambda (c: C).(\lambda (x: C).(\lambda (u: T).(\lambda (h: nat).(\lambda
236 (d: nat).(\lambda (k: K).(\lambda (H: (drop h (S d) (CHead c k u) x)).(let H0
237 \def (match H in drop return (\lambda (n: nat).(\lambda (n0: nat).(\lambda
238 (c0: C).(\lambda (c1: C).(\lambda (_: (drop n n0 c0 c1)).((eq nat n h) \to
239 ((eq nat n0 (S d)) \to ((eq C c0 (CHead c k u)) \to ((eq C c1 x) \to (ex3_2 C
240 T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_:
241 C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e: C).(\lambda (_:
242 T).(drop h (r k d) c e))))))))))))) with [(drop_refl c0) \Rightarrow (\lambda
243 (H0: (eq nat O h)).(\lambda (H1: (eq nat O (S d))).(\lambda (H2: (eq C c0
244 (CHead c k u))).(\lambda (H3: (eq C c0 x)).(eq_ind nat O (\lambda (n:
245 nat).((eq nat O (S d)) \to ((eq C c0 (CHead c k u)) \to ((eq C c0 x) \to
246 (ex3_2 C T (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda
247 (_: C).(\lambda (v: T).(eq T u (lift n (r k d) v)))) (\lambda (e: C).(\lambda
248 (_: T).(drop n (r k d) c e)))))))) (\lambda (H4: (eq nat O (S d))).(let H5
249 \def (eq_ind nat O (\lambda (e: nat).(match e in nat return (\lambda (_:
250 nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) I (S d) H4)
251 in (False_ind ((eq C c0 (CHead c k u)) \to ((eq C c0 x) \to (ex3_2 C T
252 (\lambda (e: C).(\lambda (v: T).(eq C x (CHead e k v)))) (\lambda (_:
253 C).(\lambda (v: T).(eq T u (lift O (r k d) v)))) (\lambda (e: C).(\lambda (_:
254 T).(drop O (r k d) c e)))))) H5))) h H0 H1 H2 H3))))) | (drop_drop k0 h0 c0 e
255 H0 u0) \Rightarrow (\lambda (H1: (eq nat (S h0) h)).(\lambda (H2: (eq nat O
256 (S d))).(\lambda (H3: (eq C (CHead c0 k0 u0) (CHead c k u))).(\lambda (H4:
257 (eq C e x)).(eq_ind nat (S h0) (\lambda (n: nat).((eq nat O (S d)) \to ((eq C
258 (CHead c0 k0 u0) (CHead c k u)) \to ((eq C e x) \to ((drop (r k0 h0) O c0 e)
259 \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v))))
260 (\lambda (_: C).(\lambda (v: T).(eq T u (lift n (r k d) v)))) (\lambda (e0:
261 C).(\lambda (_: T).(drop n (r k d) c e0))))))))) (\lambda (H5: (eq nat O (S
262 d))).(let H6 \def (eq_ind nat O (\lambda (e0: nat).(match e0 in nat return
263 (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
264 I (S d) H5) in (False_ind ((eq C (CHead c0 k0 u0) (CHead c k u)) \to ((eq C e
265 x) \to ((drop (r k0 h0) O c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v:
266 T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift (S
267 h0) (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop (S h0) (r k d) c
268 e0))))))) H6))) h H1 H2 H3 H4 H0))))) | (drop_skip k0 h0 d0 c0 e H0 u0)
269 \Rightarrow (\lambda (H1: (eq nat h0 h)).(\lambda (H2: (eq nat (S d0) (S
270 d))).(\lambda (H3: (eq C (CHead c0 k0 (lift h0 (r k0 d0) u0)) (CHead c k
271 u))).(\lambda (H4: (eq C (CHead e k0 u0) x)).(eq_ind nat h (\lambda (n:
272 nat).((eq nat (S d0) (S d)) \to ((eq C (CHead c0 k0 (lift n (r k0 d0) u0))
273 (CHead c k u)) \to ((eq C (CHead e k0 u0) x) \to ((drop n (r k0 d0) c0 e) \to
274 (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v))))
275 (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0:
276 C).(\lambda (_: T).(drop h (r k d) c e0))))))))) (\lambda (H5: (eq nat (S d0)
277 (S d))).(let H6 \def (f_equal nat nat (\lambda (e0: nat).(match e0 in nat
278 return (\lambda (_: nat).nat) with [O \Rightarrow d0 | (S n) \Rightarrow n]))
279 (S d0) (S d) H5) in (eq_ind nat d (\lambda (n: nat).((eq C (CHead c0 k0 (lift
280 h (r k0 n) u0)) (CHead c k u)) \to ((eq C (CHead e k0 u0) x) \to ((drop h (r
281 k0 n) c0 e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0
282 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h (r k d) v))))
283 (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))))) (\lambda (H7:
284 (eq C (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u))).(let H8 \def
285 (f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with
286 [(CSort _) \Rightarrow ((let rec lref_map (f: ((nat \to nat))) (d1: nat) (t:
287 T) on t: T \def (match t with [(TSort n) \Rightarrow (TSort n) | (TLRef i)
288 \Rightarrow (TLRef (match (blt i d1) with [true \Rightarrow i | false
289 \Rightarrow (f i)])) | (THead k1 u1 t0) \Rightarrow (THead k1 (lref_map f d1
290 u1) (lref_map f (s k1 d1) t0))]) in lref_map) (\lambda (x0: nat).(plus x0 h))
291 (r k0 d) u0) | (CHead _ _ t) \Rightarrow t])) (CHead c0 k0 (lift h (r k0 d)
292 u0)) (CHead c k u) H7) in ((let H9 \def (f_equal C K (\lambda (e0: C).(match
293 e0 in C return (\lambda (_: C).K) with [(CSort _) \Rightarrow k0 | (CHead _
294 k1 _) \Rightarrow k1])) (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7)
295 in ((let H10 \def (f_equal C C (\lambda (e0: C).(match e0 in C return
296 (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c1 _ _)
297 \Rightarrow c1])) (CHead c0 k0 (lift h (r k0 d) u0)) (CHead c k u) H7) in
298 (eq_ind C c (\lambda (c1: C).((eq K k0 k) \to ((eq T (lift h (r k0 d) u0) u)
299 \to ((eq C (CHead e k0 u0) x) \to ((drop h (r k0 d) c1 e) \to (ex3_2 C T
300 (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_:
301 C).(\lambda (v: T).(eq T u (lift h (r k d) v)))) (\lambda (e0: C).(\lambda
302 (_: T).(drop h (r k d) c e0))))))))) (\lambda (H11: (eq K k0 k)).(eq_ind K k
303 (\lambda (k1: K).((eq T (lift h (r k1 d) u0) u) \to ((eq C (CHead e k1 u0) x)
304 \to ((drop h (r k1 d) c e) \to (ex3_2 C T (\lambda (e0: C).(\lambda (v:
305 T).(eq C x (CHead e0 k v)))) (\lambda (_: C).(\lambda (v: T).(eq T u (lift h
306 (r k d) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0))))))))
307 (\lambda (H12: (eq T (lift h (r k d) u0) u)).(eq_ind T (lift h (r k d) u0)
308 (\lambda (t: T).((eq C (CHead e k u0) x) \to ((drop h (r k d) c e) \to (ex3_2
309 C T (\lambda (e0: C).(\lambda (v: T).(eq C x (CHead e0 k v)))) (\lambda (_:
310 C).(\lambda (v: T).(eq T t (lift h (r k d) v)))) (\lambda (e0: C).(\lambda
311 (_: T).(drop h (r k d) c e0))))))) (\lambda (H13: (eq C (CHead e k u0)
312 x)).(eq_ind C (CHead e k u0) (\lambda (c1: C).((drop h (r k d) c e) \to
313 (ex3_2 C T (\lambda (e0: C).(\lambda (v: T).(eq C c1 (CHead e0 k v))))
314 (\lambda (_: C).(\lambda (v: T).(eq T (lift h (r k d) u0) (lift h (r k d)
315 v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r k d) c e0)))))) (\lambda
316 (H14: (drop h (r k d) c e)).(let H15 \def (eq_ind_r T u (\lambda (t: T).(drop
317 h (S d) (CHead c k t) x)) H (lift h (r k d) u0) H12) in (let H16 \def
318 (eq_ind_r C x (\lambda (c1: C).(drop h (S d) (CHead c k (lift h (r k d) u0))
319 c1)) H15 (CHead e k u0) H13) in (ex3_2_intro C T (\lambda (e0: C).(\lambda
320 (v: T).(eq C (CHead e k u0) (CHead e0 k v)))) (\lambda (_: C).(\lambda (v:
321 T).(eq T (lift h (r k d) u0) (lift h (r k d) v)))) (\lambda (e0: C).(\lambda
322 (_: T).(drop h (r k d) c e0))) e u0 (refl_equal C (CHead e k u0)) (refl_equal
323 T (lift h (r k d) u0)) H14)))) x H13)) u H12)) k0 (sym_eq K k0 k H11))) c0
324 (sym_eq C c0 c H10))) H9)) H8))) d0 (sym_eq nat d0 d H6)))) h0 (sym_eq nat h0
325 h H1) H2 H3 H4 H0)))))]) in (H0 (refl_equal nat h) (refl_equal nat (S d))
326 (refl_equal C (CHead c k u)) (refl_equal C x))))))))).
projects / helm.git / blob