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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool_lemmas.ma".
28 include "freescale/aux_bases.ma".
34 ndefinition oct_destruct :
35 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
37 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
38 | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
39 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
40 | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
41 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
42 | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
43 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
44 | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
48 ##[ ##1: nelim n2; nnormalize; #H;
49 ##[ ##1: napply (λx:P.x)
50 ##| ##*: napply (False_ind ??);
51 nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
52 nrewrite > H; nnormalize; napply I
54 ##| ##2: nelim n2; nnormalize; #H;
55 ##[ ##2: napply (λx:P.x)
56 ##| ##*: napply (False_ind ??);
57 nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
58 nrewrite > H; nnormalize; napply I
60 ##| ##3: nelim n2; nnormalize; #H;
61 ##[ ##3: napply (λx:P.x)
62 ##| ##*: napply (False_ind ??);
63 nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
64 nrewrite > H; nnormalize; napply I
66 ##| ##4: nelim n2; nnormalize; #H;
67 ##[ ##4: napply (λx:P.x)
68 ##| ##*: napply (False_ind ??);
69 nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
70 nrewrite > H; nnormalize; napply I
72 ##| ##5: nelim n2; nnormalize; #H;
73 ##[ ##5: napply (λx:P.x)
74 ##| ##*: napply (False_ind ??);
75 nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
76 nrewrite > H; nnormalize; napply I
78 ##| ##6: nelim n2; nnormalize; #H;
79 ##[ ##6: napply (λx:P.x)
80 ##| ##*: napply (False_ind ??);
81 nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
82 nrewrite > H; nnormalize; napply I
84 ##| ##7: nelim n2; nnormalize; #H;
85 ##[ ##7: napply (λx:P.x)
86 ##| ##*: napply (False_ind ??);
87 nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
88 nrewrite > H; nnormalize; napply I
90 ##| ##8: nelim n2; nnormalize; #H;
91 ##[ ##8: napply (λx:P.x)
92 ##| ##*: napply (False_ind ??);
93 nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
94 nrewrite > H; nnormalize; napply I
99 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
107 nlemma eqoct_to_eq : ∀o1,o2.eq_oct o1 o2 = true → o1 = o2.
109 nletin K ≝ (bool_destruct ?? (n1 = n2) H);
110 nelim n1 in K:(%) ⊢ %;
113 ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
114 ##| ##*: #H; napply H
118 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
120 nletin K ≝ (oct_destruct ?? (eq_oct n1 n2 = true) H);
121 nelim n1 in K:(%) ⊢ %;
124 ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
125 ##| ##*: #H; napply H
133 ndefinition bitrigesim_destruct :
134 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
136 [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
137 | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
138 | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
139 | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
140 | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
141 | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
142 | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
143 | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
144 | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
145 | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
146 | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
147 | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
148 | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
149 | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
150 | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
151 | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
152 | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
153 | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
154 | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
155 | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
156 | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
157 | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
158 | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
159 | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
160 | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
161 | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
162 | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
163 | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
164 | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
165 | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
166 | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
167 | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
171 ##[ ##1: nelim t2; nnormalize; #H;
172 ##[ ##1: napply (λx:P.x)
173 ##| ##*: napply (False_ind ??);
174 nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
175 nrewrite > H; nnormalize; napply I
177 ##| ##2: nelim t2; nnormalize; #H;
178 ##[ ##2: napply (λx:P.x)
179 ##| ##*: napply (False_ind ??);
180 nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
181 nrewrite > H; nnormalize; napply I
183 ##| ##3: nelim t2; nnormalize; #H;
184 ##[ ##3: napply (λx:P.x)
185 ##| ##*: napply (False_ind ??);
186 nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
187 nrewrite > H; nnormalize; napply I
189 ##| ##4: nelim t2; nnormalize; #H;
190 ##[ ##4: napply (λx:P.x)
191 ##| ##*: napply (False_ind ??);
192 nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
193 nrewrite > H; nnormalize; napply I
195 ##| ##5: nelim t2; nnormalize; #H;
196 ##[ ##5: napply (λx:P.x)
197 ##| ##*: napply (False_ind ??);
198 nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
199 nrewrite > H; nnormalize; napply I
201 ##| ##6: nelim t2; nnormalize; #H;
202 ##[ ##6: napply (λx:P.x)
203 ##| ##*: napply (False_ind ??);
204 nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
205 nrewrite > H; nnormalize; napply I
207 ##| ##7: nelim t2; nnormalize; #H;
208 ##[ ##7: napply (λx:P.x)
209 ##| ##*: napply (False_ind ??);
210 nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
211 nrewrite > H; nnormalize; napply I
213 ##| ##8: nelim t2; nnormalize; #H;
214 ##[ ##8: napply (λx:P.x)
215 ##| ##*: napply (False_ind ??);
216 nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
217 nrewrite > H; nnormalize; napply I
219 ##| ##9: nelim t2; nnormalize; #H;
220 ##[ ##9: napply (λx:P.x)
221 ##| ##*: napply (False_ind ??);
222 nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
223 nrewrite > H; nnormalize; napply I
225 ##| ##10: nelim t2; nnormalize; #H;
226 ##[ ##10: napply (λx:P.x)
227 ##| ##*: napply (False_ind ??);
228 nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
229 nrewrite > H; nnormalize; napply I
231 ##| ##11: nelim t2; nnormalize; #H;
232 ##[ ##11: napply (λx:P.x)
233 ##| ##*: napply (False_ind ??);
234 nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
235 nrewrite > H; nnormalize; napply I
237 ##| ##12: nelim t2; nnormalize; #H;
238 ##[ ##12: napply (λx:P.x)
239 ##| ##*: napply (False_ind ??);
240 nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
241 nrewrite > H; nnormalize; napply I
243 ##| ##13: nelim t2; nnormalize; #H;
244 ##[ ##13: napply (λx:P.x)
245 ##| ##*: napply (False_ind ??);
246 nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
247 nrewrite > H; nnormalize; napply I
249 ##| ##14: nelim t2; nnormalize; #H;
250 ##[ ##14: napply (λx:P.x)
251 ##| ##*: napply (False_ind ??);
252 nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
253 nrewrite > H; nnormalize; napply I
255 ##| ##15: nelim t2; nnormalize; #H;
256 ##[ ##15: napply (λx:P.x)
257 ##| ##*: napply (False_ind ??);
258 nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
259 nrewrite > H; nnormalize; napply I
261 ##| ##16: nelim t2; nnormalize; #H;
262 ##[ ##16: napply (λx:P.x)
263 ##| ##*: napply (False_ind ??);
264 nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
265 nrewrite > H; nnormalize; napply I
267 ##| ##17: nelim t2; nnormalize; #H;
268 ##[ ##17: napply (λx:P.x)
269 ##| ##*: napply (False_ind ??);
270 nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
271 nrewrite > H; nnormalize; napply I
273 ##| ##18: nelim t2; nnormalize; #H;
274 ##[ ##18: napply (λx:P.x)
275 ##| ##*: napply (False_ind ??);
276 nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
277 nrewrite > H; nnormalize; napply I
279 ##| ##19: nelim t2; nnormalize; #H;
280 ##[ ##19: napply (λx:P.x)
281 ##| ##*: napply (False_ind ??);
282 nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
283 nrewrite > H; nnormalize; napply I
285 ##| ##20: nelim t2; nnormalize; #H;
286 ##[ ##20: napply (λx:P.x)
287 ##| ##*: napply (False_ind ??);
288 nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
289 nrewrite > H; nnormalize; napply I
291 ##| ##21: nelim t2; nnormalize; #H;
292 ##[ ##21: napply (λx:P.x)
293 ##| ##*: napply (False_ind ??);
294 nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
295 nrewrite > H; nnormalize; napply I
297 ##| ##22: nelim t2; nnormalize; #H;
298 ##[ ##22: napply (λx:P.x)
299 ##| ##*: napply (False_ind ??);
300 nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
301 nrewrite > H; nnormalize; napply I
303 ##| ##23: nelim t2; nnormalize; #H;
304 ##[ ##23: napply (λx:P.x)
305 ##| ##*: napply (False_ind ??);
306 nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
307 nrewrite > H; nnormalize; napply I
309 ##| ##24: nelim t2; nnormalize; #H;
310 ##[ ##24: napply (λx:P.x)
311 ##| ##*: napply (False_ind ??);
312 nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
313 nrewrite > H; nnormalize; napply I
315 ##| ##25: nelim t2; nnormalize; #H;
316 ##[ ##25: napply (λx:P.x)
317 ##| ##*: napply (False_ind ??);
318 nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
319 nrewrite > H; nnormalize; napply I
321 ##| ##26: nelim t2; nnormalize; #H;
322 ##[ ##26: napply (λx:P.x)
323 ##| ##*: napply (False_ind ??);
324 nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
325 nrewrite > H; nnormalize; napply I
327 ##| ##27: nelim t2; nnormalize; #H;
328 ##[ ##27: napply (λx:P.x)
329 ##| ##*: napply (False_ind ??);
330 nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
331 nrewrite > H; nnormalize; napply I
333 ##| ##28: nelim t2; nnormalize; #H;
334 ##[ ##28: napply (λx:P.x)
335 ##| ##*: napply (False_ind ??);
336 nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
337 nrewrite > H; nnormalize; napply I
339 ##| ##29: nelim t2; nnormalize; #H;
340 ##[ ##29: napply (λx:P.x)
341 ##| ##*: napply (False_ind ??);
342 nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
343 nrewrite > H; nnormalize; napply I
345 ##| ##30: nelim t2; nnormalize; #H;
346 ##[ ##30: napply (λx:P.x)
347 ##| ##*: napply (False_ind ??);
348 nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
349 nrewrite > H; nnormalize; napply I
351 ##| ##31: nelim t2; nnormalize; #H;
352 ##[ ##31: napply (λx:P.x)
353 ##| ##*: napply (False_ind ??);
354 nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
355 nrewrite > H; nnormalize; napply I
357 ##| ##32: nelim t2; nnormalize; #H;
358 ##[ ##32: napply (λx:P.x)
359 ##| ##*: napply (False_ind ??);
360 nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
361 nrewrite > H; nnormalize; napply I
366 nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
369 ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
370 ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
371 ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
372 ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
373 ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
374 ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
375 ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
376 ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
377 ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
378 ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
379 ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
380 ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
381 ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
382 ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
383 ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
384 ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
385 ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
386 ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
387 ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
388 ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
389 ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
390 ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
391 ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
392 ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
393 ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
394 ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
395 ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
396 ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
397 ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
398 ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
399 ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
400 ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
404 nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
406 nletin K ≝ (bool_destruct ?? (t1 = t2) H);
407 nelim t1 in K:(%) ⊢ %;
408 ##[ ##1: nelim t2; nnormalize; #H;
409 ##[ ##1: napply (refl_eq ??)
412 ##| ##2: nelim t2; nnormalize; #H;
413 ##[ ##2: napply (refl_eq ??)
416 ##| ##3: nelim t2; nnormalize; #H;
417 ##[ ##3: napply (refl_eq ??)
420 ##| ##4: nelim t2; nnormalize; #H;
421 ##[ ##4: napply (refl_eq ??)
424 ##| ##5: nelim t2; nnormalize; #H;
425 ##[ ##5: napply (refl_eq ??)
428 ##| ##6: nelim t2; nnormalize; #H;
429 ##[ ##6: napply (refl_eq ??)
432 ##| ##7: nelim t2; nnormalize; #H;
433 ##[ ##7: napply (refl_eq ??)
436 ##| ##8: nelim t2; nnormalize; #H;
437 ##[ ##8: napply (refl_eq ??)
440 ##| ##9: nelim t2; nnormalize; #H;
441 ##[ ##9: napply (refl_eq ??)
444 ##| ##10: nelim t2; nnormalize; #H;
445 ##[ ##10: napply (refl_eq ??)
448 ##| ##11: nelim t2; nnormalize; #H;
449 ##[ ##11: napply (refl_eq ??)
452 ##| ##12: nelim t2; nnormalize; #H;
453 ##[ ##12: napply (refl_eq ??)
456 ##| ##13: nelim t2; nnormalize; #H;
457 ##[ ##13: napply (refl_eq ??)
460 ##| ##14: nelim t2; nnormalize; #H;
461 ##[ ##14: napply (refl_eq ??)
464 ##| ##15: nelim t2; nnormalize; #H;
465 ##[ ##15: napply (refl_eq ??)
468 ##| ##16: nelim t2; nnormalize; #H;
469 ##[ ##16: napply (refl_eq ??)
472 ##| ##17: nelim t2; nnormalize; #H;
473 ##[ ##17: napply (refl_eq ??)
476 ##| ##18: nelim t2; nnormalize; #H;
477 ##[ ##18: napply (refl_eq ??)
480 ##| ##19: nelim t2; nnormalize; #H;
481 ##[ ##19: napply (refl_eq ??)
484 ##| ##20: nelim t2; nnormalize; #H;
485 ##[ ##20: napply (refl_eq ??)
488 ##| ##21: nelim t2; nnormalize; #H;
489 ##[ ##21: napply (refl_eq ??)
492 ##| ##22: nelim t2; nnormalize; #H;
493 ##[ ##22: napply (refl_eq ??)
496 ##| ##23: nelim t2; nnormalize; #H;
497 ##[ ##23: napply (refl_eq ??)
500 ##| ##24: nelim t2; nnormalize; #H;
501 ##[ ##24: napply (refl_eq ??)
504 ##| ##25: nelim t2; nnormalize; #H;
505 ##[ ##25: napply (refl_eq ??)
508 ##| ##26: nelim t2; nnormalize; #H;
509 ##[ ##26: napply (refl_eq ??)
512 ##| ##27: nelim t2; nnormalize; #H;
513 ##[ ##27: napply (refl_eq ??)
516 ##| ##28: nelim t2; nnormalize; #H;
517 ##[ ##28: napply (refl_eq ??)
520 ##| ##29: nelim t2; nnormalize; #H;
521 ##[ ##29: napply (refl_eq ??)
524 ##| ##30: nelim t2; nnormalize; #H;
525 ##[ ##30: napply (refl_eq ??)
528 ##| ##31: nelim t2; nnormalize; #H;
529 ##[ ##31: napply (refl_eq ??)
532 ##| ##32: nelim t2; nnormalize; #H;
533 ##[ ##32: napply (refl_eq ??)
539 nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
541 nletin K ≝ (bitrigesim_destruct ?? (eq_bitrig t1 t2 = true) H);
542 nelim t1 in K:(%) ⊢ %;
543 ##[ ##1: nelim t2; nnormalize; #H;
544 ##[ ##1: napply (refl_eq ??)
547 ##| ##2: nelim t2; nnormalize; #H;
548 ##[ ##2: napply (refl_eq ??)
551 ##| ##3: nelim t2; nnormalize; #H;
552 ##[ ##3: napply (refl_eq ??)
555 ##| ##4: nelim t2; nnormalize; #H;
556 ##[ ##4: napply (refl_eq ??)
559 ##| ##5: nelim t2; nnormalize; #H;
560 ##[ ##5: napply (refl_eq ??)
563 ##| ##6: nelim t2; nnormalize; #H;
564 ##[ ##6: napply (refl_eq ??)
567 ##| ##7: nelim t2; nnormalize; #H;
568 ##[ ##7: napply (refl_eq ??)
571 ##| ##8: nelim t2; nnormalize; #H;
572 ##[ ##8: napply (refl_eq ??)
575 ##| ##9: nelim t2; nnormalize; #H;
576 ##[ ##9: napply (refl_eq ??)
579 ##| ##10: nelim t2; nnormalize; #H;
580 ##[ ##10: napply (refl_eq ??)
583 ##| ##11: nelim t2; nnormalize; #H;
584 ##[ ##11: napply (refl_eq ??)
587 ##| ##12: nelim t2; nnormalize; #H;
588 ##[ ##12: napply (refl_eq ??)
591 ##| ##13: nelim t2; nnormalize; #H;
592 ##[ ##13: napply (refl_eq ??)
595 ##| ##14: nelim t2; nnormalize; #H;
596 ##[ ##14: napply (refl_eq ??)
599 ##| ##15: nelim t2; nnormalize; #H;
600 ##[ ##15: napply (refl_eq ??)
603 ##| ##16: nelim t2; nnormalize; #H;
604 ##[ ##16: napply (refl_eq ??)
607 ##| ##17: nelim t2; nnormalize; #H;
608 ##[ ##17: napply (refl_eq ??)
611 ##| ##18: nelim t2; nnormalize; #H;
612 ##[ ##18: napply (refl_eq ??)
615 ##| ##19: nelim t2; nnormalize; #H;
616 ##[ ##19: napply (refl_eq ??)
619 ##| ##20: nelim t2; nnormalize; #H;
620 ##[ ##20: napply (refl_eq ??)
623 ##| ##21: nelim t2; nnormalize; #H;
624 ##[ ##21: napply (refl_eq ??)
627 ##| ##22: nelim t2; nnormalize; #H;
628 ##[ ##22: napply (refl_eq ??)
631 ##| ##23: nelim t2; nnormalize; #H;
632 ##[ ##23: napply (refl_eq ??)
635 ##| ##24: nelim t2; nnormalize; #H;
636 ##[ ##24: napply (refl_eq ??)
639 ##| ##25: nelim t2; nnormalize; #H;
640 ##[ ##25: napply (refl_eq ??)
643 ##| ##26: nelim t2; nnormalize; #H;
644 ##[ ##26: napply (refl_eq ??)
647 ##| ##27: nelim t2; nnormalize; #H;
648 ##[ ##27: napply (refl_eq ??)
651 ##| ##28: nelim t2; nnormalize; #H;
652 ##[ ##28: napply (refl_eq ??)
655 ##| ##29: nelim t2; nnormalize; #H;
656 ##[ ##29: napply (refl_eq ??)
659 ##| ##30: nelim t2; nnormalize; #H;
660 ##[ ##30: napply (refl_eq ??)
663 ##| ##31: nelim t2; nnormalize; #H;
664 ##[ ##31: napply (refl_eq ??)
667 ##| ##32: nelim t2; nnormalize; #H;
668 ##[ ##32: napply (refl_eq ??)