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 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "common/ascii.ma".
25 (* ************************** *)
26 (* DEFINIZIONE ASCII MINIMALE *)
27 (* ************************** *)
29 ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ].
30 #c2; #P; ncases c2; nnormalize;
31 ##[ ##1: #H; napply (λx:P.x)
32 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
36 ndefinition ascii_destruct2 : Πc2.ΠP:Prop.ch_1 = c2 → match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ].
37 #c2; #P; ncases c2; nnormalize;
38 ##[ ##2: #H; napply (λx:P.x)
39 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
43 ndefinition ascii_destruct3 : Πc2.ΠP:Prop.ch_2 = c2 → match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ].
44 #c2; #P; ncases c2; nnormalize;
45 ##[ ##3: #H; napply (λx:P.x)
46 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
50 ndefinition ascii_destruct4 : Πc2.ΠP:Prop.ch_3 = c2 → match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ].
51 #c2; #P; ncases c2; nnormalize;
52 ##[ ##4: #H; napply (λx:P.x)
53 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
57 ndefinition ascii_destruct5 : Πc2.ΠP:Prop.ch_4 = c2 → match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ].
58 #c2; #P; ncases c2; nnormalize;
59 ##[ ##5: #H; napply (λx:P.x)
60 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
64 ndefinition ascii_destruct6 : Πc2.ΠP:Prop.ch_5 = c2 → match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ].
65 #c2; #P; ncases c2; nnormalize;
66 ##[ ##6: #H; napply (λx:P.x)
67 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
71 ndefinition ascii_destruct7 : Πc2.ΠP:Prop.ch_6 = c2 → match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ].
72 #c2; #P; ncases c2; nnormalize;
73 ##[ ##7: #H; napply (λx:P.x)
74 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
78 ndefinition ascii_destruct8 : Πc2.ΠP:Prop.ch_7 = c2 → match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ].
79 #c2; #P; ncases c2; nnormalize;
80 ##[ ##8: #H; napply (λx:P.x)
81 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
85 ndefinition ascii_destruct9 : Πc2.ΠP:Prop.ch_8 = c2 → match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ].
86 #c2; #P; ncases c2; nnormalize;
87 ##[ ##9: #H; napply (λx:P.x)
88 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
92 ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ].
93 #c2; #P; ncases c2; nnormalize;
94 ##[ ##10: #H; napply (λx:P.x)
95 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
99 ndefinition ascii_destruct11 : Πc2.ΠP:Prop.ch__ = c2 → match c2 with [ ch__ ⇒ P → P | _ ⇒ P ].
100 #c2; #P; ncases c2; nnormalize;
101 ##[ ##11: #H; napply (λx:P.x)
102 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
106 ndefinition ascii_destruct12 : Πc2.ΠP:Prop.ch_A = c2 → match c2 with [ ch_A ⇒ P → P | _ ⇒ P ].
107 #c2; #P; ncases c2; nnormalize;
108 ##[ ##12: #H; napply (λx:P.x)
109 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
113 ndefinition ascii_destruct13 : Πc2.ΠP:Prop.ch_B = c2 → match c2 with [ ch_B ⇒ P → P | _ ⇒ P ].
114 #c2; #P; ncases c2; nnormalize;
115 ##[ ##13: #H; napply (λx:P.x)
116 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
120 ndefinition ascii_destruct14 : Πc2.ΠP:Prop.ch_C = c2 → match c2 with [ ch_C ⇒ P → P | _ ⇒ P ].
121 #c2; #P; ncases c2; nnormalize;
122 ##[ ##14: #H; napply (λx:P.x)
123 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
127 ndefinition ascii_destruct15 : Πc2.ΠP:Prop.ch_D = c2 → match c2 with [ ch_D ⇒ P → P | _ ⇒ P ].
128 #c2; #P; ncases c2; nnormalize;
129 ##[ ##15: #H; napply (λx:P.x)
130 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
134 ndefinition ascii_destruct16 : Πc2.ΠP:Prop.ch_E = c2 → match c2 with [ ch_E ⇒ P → P | _ ⇒ P ].
135 #c2; #P; ncases c2; nnormalize;
136 ##[ ##16: #H; napply (λx:P.x)
137 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
141 ndefinition ascii_destruct17 : Πc2.ΠP:Prop.ch_F = c2 → match c2 with [ ch_F ⇒ P → P | _ ⇒ P ].
142 #c2; #P; ncases c2; nnormalize;
143 ##[ ##17: #H; napply (λx:P.x)
144 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
148 ndefinition ascii_destruct18 : Πc2.ΠP:Prop.ch_G = c2 → match c2 with [ ch_G ⇒ P → P | _ ⇒ P ].
149 #c2; #P; ncases c2; nnormalize;
150 ##[ ##18: #H; napply (λx:P.x)
151 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
155 ndefinition ascii_destruct19 : Πc2.ΠP:Prop.ch_H = c2 → match c2 with [ ch_H ⇒ P → P | _ ⇒ P ].
156 #c2; #P; ncases c2; nnormalize;
157 ##[ ##19: #H; napply (λx:P.x)
158 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
162 ndefinition ascii_destruct20 : Πc2.ΠP:Prop.ch_I = c2 → match c2 with [ ch_I ⇒ P → P | _ ⇒ P ].
163 #c2; #P; ncases c2; nnormalize;
164 ##[ ##20: #H; napply (λx:P.x)
165 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
169 ndefinition ascii_destruct21 : Πc2.ΠP:Prop.ch_J = c2 → match c2 with [ ch_J ⇒ P → P | _ ⇒ P ].
170 #c2; #P; ncases c2; nnormalize;
171 ##[ ##21: #H; napply (λx:P.x)
172 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
176 ndefinition ascii_destruct22 : Πc2.ΠP:Prop.ch_K = c2 → match c2 with [ ch_K ⇒ P → P | _ ⇒ P ].
177 #c2; #P; ncases c2; nnormalize;
178 ##[ ##22: #H; napply (λx:P.x)
179 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
183 ndefinition ascii_destruct23 : Πc2.ΠP:Prop.ch_L = c2 → match c2 with [ ch_L ⇒ P → P | _ ⇒ P ].
184 #c2; #P; ncases c2; nnormalize;
185 ##[ ##23: #H; napply (λx:P.x)
186 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
190 ndefinition ascii_destruct24 : Πc2.ΠP:Prop.ch_M = c2 → match c2 with [ ch_M ⇒ P → P | _ ⇒ P ].
191 #c2; #P; ncases c2; nnormalize;
192 ##[ ##24: #H; napply (λx:P.x)
193 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
197 ndefinition ascii_destruct25 : Πc2.ΠP:Prop.ch_N = c2 → match c2 with [ ch_N ⇒ P → P | _ ⇒ P ].
198 #c2; #P; ncases c2; nnormalize;
199 ##[ ##25: #H; napply (λx:P.x)
200 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
204 ndefinition ascii_destruct26 : Πc2.ΠP:Prop.ch_O = c2 → match c2 with [ ch_O ⇒ P → P | _ ⇒ P ].
205 #c2; #P; ncases c2; nnormalize;
206 ##[ ##26: #H; napply (λx:P.x)
207 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
211 ndefinition ascii_destruct27 : Πc2.ΠP:Prop.ch_P = c2 → match c2 with [ ch_P ⇒ P → P | _ ⇒ P ].
212 #c2; #P; ncases c2; nnormalize;
213 ##[ ##27: #H; napply (λx:P.x)
214 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
218 ndefinition ascii_destruct28 : Πc2.ΠP:Prop.ch_Q = c2 → match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ].
219 #c2; #P; ncases c2; nnormalize;
220 ##[ ##28: #H; napply (λx:P.x)
221 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
225 ndefinition ascii_destruct29 : Πc2.ΠP:Prop.ch_R = c2 → match c2 with [ ch_R ⇒ P → P | _ ⇒ P ].
226 #c2; #P; ncases c2; nnormalize;
227 ##[ ##29: #H; napply (λx:P.x)
228 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
232 ndefinition ascii_destruct30 : Πc2.ΠP:Prop.ch_S = c2 → match c2 with [ ch_S ⇒ P → P | _ ⇒ P ].
233 #c2; #P; ncases c2; nnormalize;
234 ##[ ##30: #H; napply (λx:P.x)
235 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
239 ndefinition ascii_destruct31 : Πc2.ΠP:Prop.ch_T = c2 → match c2 with [ ch_T ⇒ P → P | _ ⇒ P ].
240 #c2; #P; ncases c2; nnormalize;
241 ##[ ##31: #H; napply (λx:P.x)
242 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
246 ndefinition ascii_destruct32 : Πc2.ΠP:Prop.ch_U = c2 → match c2 with [ ch_U ⇒ P → P | _ ⇒ P ].
247 #c2; #P; ncases c2; nnormalize;
248 ##[ ##32: #H; napply (λx:P.x)
249 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
253 ndefinition ascii_destruct33 : Πc2.ΠP:Prop.ch_V = c2 → match c2 with [ ch_V ⇒ P → P | _ ⇒ P ].
254 #c2; #P; ncases c2; nnormalize;
255 ##[ ##33: #H; napply (λx:P.x)
256 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
260 ndefinition ascii_destruct34 : Πc2.ΠP:Prop.ch_W = c2 → match c2 with [ ch_W ⇒ P → P | _ ⇒ P ].
261 #c2; #P; ncases c2; nnormalize;
262 ##[ ##34: #H; napply (λx:P.x)
263 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
267 ndefinition ascii_destruct35 : Πc2.ΠP:Prop.ch_X = c2 → match c2 with [ ch_X ⇒ P → P | _ ⇒ P ].
268 #c2; #P; ncases c2; nnormalize;
269 ##[ ##35: #H; napply (λx:P.x)
270 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
274 ndefinition ascii_destruct36 : Πc2.ΠP:Prop.ch_Y = c2 → match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ].
275 #c2; #P; ncases c2; nnormalize;
276 ##[ ##36: #H; napply (λx:P.x)
277 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
281 ndefinition ascii_destruct37 : Πc2.ΠP:Prop.ch_Z = c2 → match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ].
282 #c2; #P; ncases c2; nnormalize;
283 ##[ ##37: #H; napply (λx:P.x)
284 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
288 ndefinition ascii_destruct38 : Πc2.ΠP:Prop.ch_a = c2 → match c2 with [ ch_a ⇒ P → P | _ ⇒ P ].
289 #c2; #P; ncases c2; nnormalize;
290 ##[ ##38: #H; napply (λx:P.x)
291 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
295 ndefinition ascii_destruct39 : Πc2.ΠP:Prop.ch_b = c2 → match c2 with [ ch_b ⇒ P → P | _ ⇒ P ].
296 #c2; #P; ncases c2; nnormalize;
297 ##[ ##39: #H; napply (λx:P.x)
298 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
302 ndefinition ascii_destruct40 : Πc2.ΠP:Prop.ch_c = c2 → match c2 with [ ch_c ⇒ P → P | _ ⇒ P ].
303 #c2; #P; ncases c2; nnormalize;
304 ##[ ##40: #H; napply (λx:P.x)
305 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
309 ndefinition ascii_destruct41 : Πc2.ΠP:Prop.ch_d = c2 → match c2 with [ ch_d ⇒ P → P | _ ⇒ P ].
310 #c2; #P; ncases c2; nnormalize;
311 ##[ ##41: #H; napply (λx:P.x)
312 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
316 ndefinition ascii_destruct42 : Πc2.ΠP:Prop.ch_e = c2 → match c2 with [ ch_e ⇒ P → P | _ ⇒ P ].
317 #c2; #P; ncases c2; nnormalize;
318 ##[ ##42: #H; napply (λx:P.x)
319 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
323 ndefinition ascii_destruct43 : Πc2.ΠP:Prop.ch_f = c2 → match c2 with [ ch_f ⇒ P → P | _ ⇒ P ].
324 #c2; #P; ncases c2; nnormalize;
325 ##[ ##43: #H; napply (λx:P.x)
326 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
330 ndefinition ascii_destruct44 : Πc2.ΠP:Prop.ch_g = c2 → match c2 with [ ch_g ⇒ P → P | _ ⇒ P ].
331 #c2; #P; ncases c2; nnormalize;
332 ##[ ##44: #H; napply (λx:P.x)
333 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
337 ndefinition ascii_destruct45 : Πc2.ΠP:Prop.ch_h = c2 → match c2 with [ ch_h ⇒ P → P | _ ⇒ P ].
338 #c2; #P; ncases c2; nnormalize;
339 ##[ ##45: #H; napply (λx:P.x)
340 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
344 ndefinition ascii_destruct46 : Πc2.ΠP:Prop.ch_i = c2 → match c2 with [ ch_i ⇒ P → P | _ ⇒ P ].
345 #c2; #P; ncases c2; nnormalize;
346 ##[ ##46: #H; napply (λx:P.x)
347 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
351 ndefinition ascii_destruct47 : Πc2.ΠP:Prop.ch_j = c2 → match c2 with [ ch_j ⇒ P → P | _ ⇒ P ].
352 #c2; #P; ncases c2; nnormalize;
353 ##[ ##47: #H; napply (λx:P.x)
354 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
358 ndefinition ascii_destruct48 : Πc2.ΠP:Prop.ch_k = c2 → match c2 with [ ch_k ⇒ P → P | _ ⇒ P ].
359 #c2; #P; ncases c2; nnormalize;
360 ##[ ##48: #H; napply (λx:P.x)
361 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
365 ndefinition ascii_destruct49 : Πc2.ΠP:Prop.ch_l = c2 → match c2 with [ ch_l ⇒ P → P | _ ⇒ P ].
366 #c2; #P; ncases c2; nnormalize;
367 ##[ ##49: #H; napply (λx:P.x)
368 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
372 ndefinition ascii_destruct50 : Πc2.ΠP:Prop.ch_m = c2 → match c2 with [ ch_m ⇒ P → P | _ ⇒ P ].
373 #c2; #P; ncases c2; nnormalize;
374 ##[ ##50: #H; napply (λx:P.x)
375 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
379 ndefinition ascii_destruct51 : Πc2.ΠP:Prop.ch_n = c2 → match c2 with [ ch_n ⇒ P → P | _ ⇒ P ].
380 #c2; #P; ncases c2; nnormalize;
381 ##[ ##51: #H; napply (λx:P.x)
382 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
386 ndefinition ascii_destruct52 : Πc2.ΠP:Prop.ch_o = c2 → match c2 with [ ch_o ⇒ P → P | _ ⇒ P ].
387 #c2; #P; ncases c2; nnormalize;
388 ##[ ##52: #H; napply (λx:P.x)
389 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
393 ndefinition ascii_destruct53 : Πc2.ΠP:Prop.ch_p = c2 → match c2 with [ ch_p ⇒ P → P | _ ⇒ P ].
394 #c2; #P; ncases c2; nnormalize;
395 ##[ ##53: #H; napply (λx:P.x)
396 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
400 ndefinition ascii_destruct54 : Πc2.ΠP:Prop.ch_q = c2 → match c2 with [ ch_q ⇒ P → P | _ ⇒ P ].
401 #c2; #P; ncases c2; nnormalize;
402 ##[ ##54: #H; napply (λx:P.x)
403 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
407 ndefinition ascii_destruct55 : Πc2.ΠP:Prop.ch_r = c2 → match c2 with [ ch_r ⇒ P → P | _ ⇒ P ].
408 #c2; #P; ncases c2; nnormalize;
409 ##[ ##55: #H; napply (λx:P.x)
410 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
414 ndefinition ascii_destruct56 : Πc2.ΠP:Prop.ch_s = c2 → match c2 with [ ch_s ⇒ P → P | _ ⇒ P ].
415 #c2; #P; ncases c2; nnormalize;
416 ##[ ##56: #H; napply (λx:P.x)
417 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
421 ndefinition ascii_destruct57 : Πc2.ΠP:Prop.ch_t = c2 → match c2 with [ ch_t ⇒ P → P | _ ⇒ P ].
422 #c2; #P; ncases c2; nnormalize;
423 ##[ ##57: #H; napply (λx:P.x)
424 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
428 ndefinition ascii_destruct58 : Πc2.ΠP:Prop.ch_u = c2 → match c2 with [ ch_u ⇒ P → P | _ ⇒ P ].
429 #c2; #P; ncases c2; nnormalize;
430 ##[ ##58: #H; napply (λx:P.x)
431 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
435 ndefinition ascii_destruct59 : Πc2.ΠP:Prop.ch_v = c2 → match c2 with [ ch_v ⇒ P → P | _ ⇒ P ].
436 #c2; #P; ncases c2; nnormalize;
437 ##[ ##59: #H; napply (λx:P.x)
438 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
442 ndefinition ascii_destruct60 : Πc2.ΠP:Prop.ch_w = c2 → match c2 with [ ch_w ⇒ P → P | _ ⇒ P ].
443 #c2; #P; ncases c2; nnormalize;
444 ##[ ##60: #H; napply (λx:P.x)
445 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
449 ndefinition ascii_destruct61 : Πc2.ΠP:Prop.ch_x = c2 → match c2 with [ ch_x ⇒ P → P | _ ⇒ P ].
450 #c2; #P; ncases c2; nnormalize;
451 ##[ ##61: #H; napply (λx:P.x)
452 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
456 ndefinition ascii_destruct62 : Πc2.ΠP:Prop.ch_y = c2 → match c2 with [ ch_y ⇒ P → P | _ ⇒ P ].
457 #c2; #P; ncases c2; nnormalize;
458 ##[ ##62: #H; napply (λx:P.x)
459 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
463 ndefinition ascii_destruct63 : Πc2.ΠP:Prop.ch_z = c2 → match c2 with [ ch_z ⇒ P → P | _ ⇒ P ].
464 #c2; #P; ncases c2; nnormalize;
465 ##[ ##63: #H; napply (λx:P.x)
466 ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
470 ndefinition ascii_destruct_aux ≝
471 Πc1,c2.ΠP:Prop.c1 = c2 →
473 [ ch_0 ⇒ match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ] | ch_1 ⇒ match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ]
474 | ch_2 ⇒ match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ] | ch_3 ⇒ match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ]
475 | ch_4 ⇒ match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ] | ch_5 ⇒ match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ]
476 | ch_6 ⇒ match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ] | ch_7 ⇒ match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ]
477 | ch_8 ⇒ match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ] | ch_9 ⇒ match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ]
478 | ch__ ⇒ match c2 with [ ch__ ⇒ P → P | _ ⇒ P ] | ch_A ⇒ match c2 with [ ch_A ⇒ P → P | _ ⇒ P ]
479 | ch_B ⇒ match c2 with [ ch_B ⇒ P → P | _ ⇒ P ] | ch_C ⇒ match c2 with [ ch_C ⇒ P → P | _ ⇒ P ]
480 | ch_D ⇒ match c2 with [ ch_D ⇒ P → P | _ ⇒ P ] | ch_E ⇒ match c2 with [ ch_E ⇒ P → P | _ ⇒ P ]
481 | ch_F ⇒ match c2 with [ ch_F ⇒ P → P | _ ⇒ P ] | ch_G ⇒ match c2 with [ ch_G ⇒ P → P | _ ⇒ P ]
482 | ch_H ⇒ match c2 with [ ch_H ⇒ P → P | _ ⇒ P ] | ch_I ⇒ match c2 with [ ch_I ⇒ P → P | _ ⇒ P ]
483 | ch_J ⇒ match c2 with [ ch_J ⇒ P → P | _ ⇒ P ] | ch_K ⇒ match c2 with [ ch_K ⇒ P → P | _ ⇒ P ]
484 | ch_L ⇒ match c2 with [ ch_L ⇒ P → P | _ ⇒ P ] | ch_M ⇒ match c2 with [ ch_M ⇒ P → P | _ ⇒ P ]
485 | ch_N ⇒ match c2 with [ ch_N ⇒ P → P | _ ⇒ P ] | ch_O ⇒ match c2 with [ ch_O ⇒ P → P | _ ⇒ P ]
486 | ch_P ⇒ match c2 with [ ch_P ⇒ P → P | _ ⇒ P ] | ch_Q ⇒ match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ]
487 | ch_R ⇒ match c2 with [ ch_R ⇒ P → P | _ ⇒ P ] | ch_S ⇒ match c2 with [ ch_S ⇒ P → P | _ ⇒ P ]
488 | ch_T ⇒ match c2 with [ ch_T ⇒ P → P | _ ⇒ P ] | ch_U ⇒ match c2 with [ ch_U ⇒ P → P | _ ⇒ P ]
489 | ch_V ⇒ match c2 with [ ch_V ⇒ P → P | _ ⇒ P ] | ch_W ⇒ match c2 with [ ch_W ⇒ P → P | _ ⇒ P ]
490 | ch_X ⇒ match c2 with [ ch_X ⇒ P → P | _ ⇒ P ] | ch_Y ⇒ match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ]
491 | ch_Z ⇒ match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ] | ch_a ⇒ match c2 with [ ch_a ⇒ P → P | _ ⇒ P ]
492 | ch_b ⇒ match c2 with [ ch_b ⇒ P → P | _ ⇒ P ] | ch_c ⇒ match c2 with [ ch_c ⇒ P → P | _ ⇒ P ]
493 | ch_d ⇒ match c2 with [ ch_d ⇒ P → P | _ ⇒ P ] | ch_e ⇒ match c2 with [ ch_e ⇒ P → P | _ ⇒ P ]
494 | ch_f ⇒ match c2 with [ ch_f ⇒ P → P | _ ⇒ P ] | ch_g ⇒ match c2 with [ ch_g ⇒ P → P | _ ⇒ P ]
495 | ch_h ⇒ match c2 with [ ch_h ⇒ P → P | _ ⇒ P ] | ch_i ⇒ match c2 with [ ch_i ⇒ P → P | _ ⇒ P ]
496 | ch_j ⇒ match c2 with [ ch_j ⇒ P → P | _ ⇒ P ] | ch_k ⇒ match c2 with [ ch_k ⇒ P → P | _ ⇒ P ]
497 | ch_l ⇒ match c2 with [ ch_l ⇒ P → P | _ ⇒ P ] | ch_m ⇒ match c2 with [ ch_m ⇒ P → P | _ ⇒ P ]
498 | ch_n ⇒ match c2 with [ ch_n ⇒ P → P | _ ⇒ P ] | ch_o ⇒ match c2 with [ ch_o ⇒ P → P | _ ⇒ P ]
499 | ch_p ⇒ match c2 with [ ch_p ⇒ P → P | _ ⇒ P ] | ch_q ⇒ match c2 with [ ch_q ⇒ P → P | _ ⇒ P ]
500 | ch_r ⇒ match c2 with [ ch_r ⇒ P → P | _ ⇒ P ] | ch_s ⇒ match c2 with [ ch_s ⇒ P → P | _ ⇒ P ]
501 | ch_t ⇒ match c2 with [ ch_t ⇒ P → P | _ ⇒ P ] | ch_u ⇒ match c2 with [ ch_u ⇒ P → P | _ ⇒ P ]
502 | ch_v ⇒ match c2 with [ ch_v ⇒ P → P | _ ⇒ P ] | ch_w ⇒ match c2 with [ ch_w ⇒ P → P | _ ⇒ P ]
503 | ch_x ⇒ match c2 with [ ch_x ⇒ P → P | _ ⇒ P ] | ch_y ⇒ match c2 with [ ch_y ⇒ P → P | _ ⇒ P ]
504 | ch_z ⇒ match c2 with [ ch_z ⇒ P → P | _ ⇒ P ]].
506 nlemma ascii_destruct : ascii_destruct_aux.
508 ##[ ##1: napply ascii_destruct1 ##| ##2: napply ascii_destruct2
509 ##| ##3: napply ascii_destruct3 ##| ##4: napply ascii_destruct4
510 ##| ##5: napply ascii_destruct5 ##| ##6: napply ascii_destruct6
511 ##| ##7: napply ascii_destruct7 ##| ##8: napply ascii_destruct8
512 ##| ##9: napply ascii_destruct9 ##| ##10: napply ascii_destruct10
513 ##| ##11: napply ascii_destruct11 ##| ##12: napply ascii_destruct12
514 ##| ##13: napply ascii_destruct13 ##| ##14: napply ascii_destruct14
515 ##| ##15: napply ascii_destruct15 ##| ##16: napply ascii_destruct16
516 ##| ##17: napply ascii_destruct17 ##| ##18: napply ascii_destruct18
517 ##| ##19: napply ascii_destruct19 ##| ##20: napply ascii_destruct20
518 ##| ##21: napply ascii_destruct21 ##| ##22: napply ascii_destruct22
519 ##| ##23: napply ascii_destruct23 ##| ##24: napply ascii_destruct24
520 ##| ##25: napply ascii_destruct25 ##| ##26: napply ascii_destruct26
521 ##| ##27: napply ascii_destruct27 ##| ##28: napply ascii_destruct28
522 ##| ##29: napply ascii_destruct29 ##| ##30: napply ascii_destruct30
523 ##| ##31: napply ascii_destruct31 ##| ##32: napply ascii_destruct32
524 ##| ##33: napply ascii_destruct33 ##| ##34: napply ascii_destruct34
525 ##| ##35: napply ascii_destruct35 ##| ##36: napply ascii_destruct36
526 ##| ##37: napply ascii_destruct37 ##| ##38: napply ascii_destruct38
527 ##| ##39: napply ascii_destruct39 ##| ##40: napply ascii_destruct40
528 ##| ##41: napply ascii_destruct41 ##| ##42: napply ascii_destruct42
529 ##| ##43: napply ascii_destruct43 ##| ##44: napply ascii_destruct44
530 ##| ##45: napply ascii_destruct45 ##| ##46: napply ascii_destruct46
531 ##| ##47: napply ascii_destruct47 ##| ##48: napply ascii_destruct48
532 ##| ##49: napply ascii_destruct49 ##| ##50: napply ascii_destruct50
533 ##| ##51: napply ascii_destruct51 ##| ##52: napply ascii_destruct52
534 ##| ##53: napply ascii_destruct53 ##| ##54: napply ascii_destruct54
535 ##| ##55: napply ascii_destruct55 ##| ##56: napply ascii_destruct56
536 ##| ##57: napply ascii_destruct57 ##| ##58: napply ascii_destruct58
537 ##| ##59: napply ascii_destruct59 ##| ##60: napply ascii_destruct60
538 ##| ##61: napply ascii_destruct61 ##| ##62: napply ascii_destruct62
539 ##| ##63: napply ascii_destruct63 ##]