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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/bitrigesim.ma".
24 include "num/bool_lemmas.ma".
30 ndefinition bitrigesim_destruct1 :
31 Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
35 ##[ ##1: napply (λx:P.x)
36 ##| ##*: napply False_ind;
37 nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
38 nrewrite > H; nnormalize; napply I
42 ndefinition bitrigesim_destruct2 :
43 Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
47 ##[ ##2: napply (λx:P.x)
48 ##| ##*: napply False_ind;
49 nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
50 nrewrite > H; nnormalize; napply I
54 ndefinition bitrigesim_destruct3 :
55 Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
59 ##[ ##3: napply (λx:P.x)
60 ##| ##*: napply False_ind;
61 nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
62 nrewrite > H; nnormalize; napply I
66 ndefinition bitrigesim_destruct4 :
67 Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
71 ##[ ##4: napply (λx:P.x)
72 ##| ##*: napply False_ind;
73 nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
74 nrewrite > H; nnormalize; napply I
78 ndefinition bitrigesim_destruct5 :
79 Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
83 ##[ ##5: napply (λx:P.x)
84 ##| ##*: napply False_ind;
85 nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
86 nrewrite > H; nnormalize; napply I
90 ndefinition bitrigesim_destruct6 :
91 Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
95 ##[ ##6: napply (λx:P.x)
96 ##| ##*: napply False_ind;
97 nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
98 nrewrite > H; nnormalize; napply I
102 ndefinition bitrigesim_destruct7 :
103 Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
107 ##[ ##7: napply (λx:P.x)
108 ##| ##*: napply False_ind;
109 nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
110 nrewrite > H; nnormalize; napply I
114 ndefinition bitrigesim_destruct8 :
115 Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
119 ##[ ##8: napply (λx:P.x)
120 ##| ##*: napply False_ind;
121 nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
122 nrewrite > H; nnormalize; napply I
126 ndefinition bitrigesim_destruct9 :
127 Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
131 ##[ ##9: napply (λx:P.x)
132 ##| ##*: napply False_ind;
133 nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
134 nrewrite > H; nnormalize; napply I
138 ndefinition bitrigesim_destruct10 :
139 Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
143 ##[ ##10: napply (λx:P.x)
144 ##| ##*: napply False_ind;
145 nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
146 nrewrite > H; nnormalize; napply I
150 ndefinition bitrigesim_destruct11 :
151 Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
155 ##[ ##11: napply (λx:P.x)
156 ##| ##*: napply False_ind;
157 nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
158 nrewrite > H; nnormalize; napply I
162 ndefinition bitrigesim_destruct12 :
163 Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
167 ##[ ##12: napply (λx:P.x)
168 ##| ##*: napply False_ind;
169 nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
170 nrewrite > H; nnormalize; napply I
174 ndefinition bitrigesim_destruct13 :
175 Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
179 ##[ ##13: napply (λx:P.x)
180 ##| ##*: napply False_ind;
181 nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
182 nrewrite > H; nnormalize; napply I
186 ndefinition bitrigesim_destruct14 :
187 Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
191 ##[ ##14: napply (λx:P.x)
192 ##| ##*: napply False_ind;
193 nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
194 nrewrite > H; nnormalize; napply I
198 ndefinition bitrigesim_destruct15 :
199 Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
203 ##[ ##15: napply (λx:P.x)
204 ##| ##*: napply False_ind;
205 nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
206 nrewrite > H; nnormalize; napply I
210 ndefinition bitrigesim_destruct16 :
211 Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
215 ##[ ##16: napply (λx:P.x)
216 ##| ##*: napply False_ind;
217 nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
218 nrewrite > H; nnormalize; napply I
222 ndefinition bitrigesim_destruct17 :
223 Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
227 ##[ ##17: napply (λx:P.x)
228 ##| ##*: napply False_ind;
229 nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
230 nrewrite > H; nnormalize; napply I
234 ndefinition bitrigesim_destruct18 :
235 Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
239 ##[ ##18: napply (λx:P.x)
240 ##| ##*: napply False_ind;
241 nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
242 nrewrite > H; nnormalize; napply I
246 ndefinition bitrigesim_destruct19 :
247 Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
251 ##[ ##19: napply (λx:P.x)
252 ##| ##*: napply False_ind;
253 nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
254 nrewrite > H; nnormalize; napply I
258 ndefinition bitrigesim_destruct20 :
259 Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
263 ##[ ##20: napply (λx:P.x)
264 ##| ##*: napply False_ind;
265 nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
266 nrewrite > H; nnormalize; napply I
270 ndefinition bitrigesim_destruct21 :
271 Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
275 ##[ ##21: napply (λx:P.x)
276 ##| ##*: napply False_ind;
277 nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
278 nrewrite > H; nnormalize; napply I
282 ndefinition bitrigesim_destruct22 :
283 Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
287 ##[ ##22: napply (λx:P.x)
288 ##| ##*: napply False_ind;
289 nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
290 nrewrite > H; nnormalize; napply I
294 ndefinition bitrigesim_destruct23 :
295 Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
299 ##[ ##23: napply (λx:P.x)
300 ##| ##*: napply False_ind;
301 nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
302 nrewrite > H; nnormalize; napply I
306 ndefinition bitrigesim_destruct24 :
307 Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
311 ##[ ##24: napply (λx:P.x)
312 ##| ##*: napply False_ind;
313 nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
314 nrewrite > H; nnormalize; napply I
318 ndefinition bitrigesim_destruct25 :
319 Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
323 ##[ ##25: napply (λx:P.x)
324 ##| ##*: napply False_ind;
325 nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
326 nrewrite > H; nnormalize; napply I
330 ndefinition bitrigesim_destruct26 :
331 Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
335 ##[ ##26: napply (λx:P.x)
336 ##| ##*: napply False_ind;
337 nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
338 nrewrite > H; nnormalize; napply I
342 ndefinition bitrigesim_destruct27 :
343 Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
347 ##[ ##27: napply (λx:P.x)
348 ##| ##*: napply False_ind;
349 nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
350 nrewrite > H; nnormalize; napply I
354 ndefinition bitrigesim_destruct28 :
355 Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
359 ##[ ##28: napply (λx:P.x)
360 ##| ##*: napply False_ind;
361 nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
362 nrewrite > H; nnormalize; napply I
366 ndefinition bitrigesim_destruct29 :
367 Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
371 ##[ ##29: napply (λx:P.x)
372 ##| ##*: napply False_ind;
373 nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
374 nrewrite > H; nnormalize; napply I
378 ndefinition bitrigesim_destruct30 :
379 Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
383 ##[ ##30: napply (λx:P.x)
384 ##| ##*: napply False_ind;
385 nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
386 nrewrite > H; nnormalize; napply I
390 ndefinition bitrigesim_destruct31 :
391 Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
395 ##[ ##31: napply (λx:P.x)
396 ##| ##*: napply False_ind;
397 nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
398 nrewrite > H; nnormalize; napply I
402 ndefinition bitrigesim_destruct32 :
403 Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
407 ##[ ##32: napply (λx:P.x)
408 ##| ##*: napply False_ind;
409 nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
410 nrewrite > H; nnormalize; napply I
414 ndefinition bitrigesim_destruct_aux ≝
415 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
417 [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
418 | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
419 | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
420 | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
421 | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
422 | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
423 | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
424 | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
425 | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
426 | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
427 | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
428 | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
429 | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
430 | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
431 | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
432 | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
435 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
438 ##[ ##1: napply bitrigesim_destruct1 ##| ##2: napply bitrigesim_destruct2
439 ##| ##3: napply bitrigesim_destruct3 ##| ##4: napply bitrigesim_destruct4
440 ##| ##5: napply bitrigesim_destruct5 ##| ##6: napply bitrigesim_destruct6
441 ##| ##7: napply bitrigesim_destruct7 ##| ##8: napply bitrigesim_destruct8
442 ##| ##9: napply bitrigesim_destruct9 ##| ##10: napply bitrigesim_destruct10
443 ##| ##11: napply bitrigesim_destruct11 ##| ##12: napply bitrigesim_destruct12
444 ##| ##13: napply bitrigesim_destruct13 ##| ##14: napply bitrigesim_destruct14
445 ##| ##15: napply bitrigesim_destruct15 ##| ##16: napply bitrigesim_destruct16
446 ##| ##17: napply bitrigesim_destruct17 ##| ##18: napply bitrigesim_destruct18
447 ##| ##19: napply bitrigesim_destruct19 ##| ##20: napply bitrigesim_destruct20
448 ##| ##21: napply bitrigesim_destruct21 ##| ##22: napply bitrigesim_destruct22
449 ##| ##23: napply bitrigesim_destruct23 ##| ##24: napply bitrigesim_destruct24
450 ##| ##25: napply bitrigesim_destruct25 ##| ##26: napply bitrigesim_destruct26
451 ##| ##27: napply bitrigesim_destruct27 ##| ##28: napply bitrigesim_destruct28
452 ##| ##29: napply bitrigesim_destruct29 ##| ##30: napply bitrigesim_destruct30
453 ##| ##31: napply bitrigesim_destruct31 ##| ##32: napply bitrigesim_destruct32
457 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
460 ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
461 ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
462 ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
463 ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
464 ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
465 ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
466 ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
467 ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
468 ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
469 ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
470 ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
471 ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
472 ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
473 ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
474 ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
475 ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
476 ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
477 ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
478 ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
479 ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
480 ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
481 ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
482 ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
483 ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
484 ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
485 ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
486 ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
487 ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
488 ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
489 ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
490 ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
491 ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
495 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
496 #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
499 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
500 #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
503 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
504 #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
507 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
508 #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
511 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
512 #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
515 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
516 #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
519 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
520 #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
523 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
524 #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
527 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
528 #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
531 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
532 #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
535 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
536 #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
539 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
540 #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
543 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
544 #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
547 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
548 #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
551 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
552 #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
555 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
556 #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
559 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
560 #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
563 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
564 #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
567 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
568 #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
571 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
572 #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
575 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
576 #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
579 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
580 #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
583 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
584 #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
587 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
588 #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
591 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
592 #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
595 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
596 #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
599 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
600 #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
603 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
604 #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
607 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
608 #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
611 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
612 #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
615 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
616 #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
619 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
620 #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
623 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
625 ##[ ##1: napply eqbit_to_eq1 ##| ##2: napply eqbit_to_eq2
626 ##| ##3: napply eqbit_to_eq3 ##| ##4: napply eqbit_to_eq4
627 ##| ##5: napply eqbit_to_eq5 ##| ##6: napply eqbit_to_eq6
628 ##| ##7: napply eqbit_to_eq7 ##| ##8: napply eqbit_to_eq8
629 ##| ##9: napply eqbit_to_eq9 ##| ##10: napply eqbit_to_eq10
630 ##| ##11: napply eqbit_to_eq11 ##| ##12: napply eqbit_to_eq12
631 ##| ##13: napply eqbit_to_eq13 ##| ##14: napply eqbit_to_eq14
632 ##| ##15: napply eqbit_to_eq15 ##| ##16: napply eqbit_to_eq16
633 ##| ##17: napply eqbit_to_eq17 ##| ##18: napply eqbit_to_eq18
634 ##| ##19: napply eqbit_to_eq19 ##| ##20: napply eqbit_to_eq20
635 ##| ##21: napply eqbit_to_eq21 ##| ##22: napply eqbit_to_eq22
636 ##| ##23: napply eqbit_to_eq23 ##| ##24: napply eqbit_to_eq24
637 ##| ##25: napply eqbit_to_eq25 ##| ##26: napply eqbit_to_eq26
638 ##| ##27: napply eqbit_to_eq27 ##| ##28: napply eqbit_to_eq28
639 ##| ##29: napply eqbit_to_eq29 ##| ##30: napply eqbit_to_eq30
640 ##| ##31: napply eqbit_to_eq31 ##| ##32: napply eqbit_to_eq32
644 nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
645 #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
648 nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
649 #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
652 nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
653 #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
656 nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
657 #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
660 nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
661 #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
664 nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
665 #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
668 nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
669 #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
672 nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
673 #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
676 nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
677 #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
680 nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
681 #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
684 nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
685 #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
688 nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
689 #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
692 nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
693 #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
696 nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
697 #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
700 nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
701 #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
704 nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
705 #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
708 nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
709 #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
712 nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
713 #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
716 nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
717 #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
720 nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
721 #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
724 nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
725 #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
728 nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
729 #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
732 nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
733 #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
736 nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
737 #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
740 nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
741 #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
744 nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
745 #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
748 nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
749 #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
752 nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
753 #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
756 nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
757 #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
760 nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
761 #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
764 nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
765 #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
768 nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
769 #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
772 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
774 ##[ ##1: napply eq_to_eqbit1 ##| ##2: napply eq_to_eqbit2
775 ##| ##3: napply eq_to_eqbit3 ##| ##4: napply eq_to_eqbit4
776 ##| ##5: napply eq_to_eqbit5 ##| ##6: napply eq_to_eqbit6
777 ##| ##7: napply eq_to_eqbit7 ##| ##8: napply eq_to_eqbit8
778 ##| ##9: napply eq_to_eqbit9 ##| ##10: napply eq_to_eqbit10
779 ##| ##11: napply eq_to_eqbit11 ##| ##12: napply eq_to_eqbit12
780 ##| ##13: napply eq_to_eqbit13 ##| ##14: napply eq_to_eqbit14
781 ##| ##15: napply eq_to_eqbit15 ##| ##16: napply eq_to_eqbit16
782 ##| ##17: napply eq_to_eqbit17 ##| ##18: napply eq_to_eqbit18
783 ##| ##19: napply eq_to_eqbit19 ##| ##20: napply eq_to_eqbit20
784 ##| ##21: napply eq_to_eqbit21 ##| ##22: napply eq_to_eqbit22
785 ##| ##23: napply eq_to_eqbit23 ##| ##24: napply eq_to_eqbit24
786 ##| ##25: napply eq_to_eqbit25 ##| ##26: napply eq_to_eqbit26
787 ##| ##27: napply eq_to_eqbit27 ##| ##28: napply eq_to_eqbit28
788 ##| ##29: napply eq_to_eqbit29 ##| ##30: napply eq_to_eqbit30
789 ##| ##31: napply eq_to_eqbit31 ##| ##32: napply eq_to_eqbit32
793 nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
794 #x; nnormalize; nelim x;
795 ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
796 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
800 nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
801 #x; nnormalize; nelim x;
802 ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
803 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
807 nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
808 #x; nnormalize; nelim x;
809 ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
810 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
814 nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
815 #x; nnormalize; nelim x;
816 ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
817 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
821 nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
822 #x; nnormalize; nelim x;
823 ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
824 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
828 nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
829 #x; nnormalize; nelim x;
830 ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
831 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
835 nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
836 #x; nnormalize; nelim x;
837 ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
838 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
842 nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
843 #x; nnormalize; nelim x;
844 ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
845 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
849 nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
850 #x; nnormalize; nelim x;
851 ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
852 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
856 nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
857 #x; nnormalize; nelim x;
858 ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
859 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
863 nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
864 #x; nnormalize; nelim x;
865 ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
866 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
870 nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
871 #x; nnormalize; nelim x;
872 ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
873 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
877 nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
878 #x; nnormalize; nelim x;
879 ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
880 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
884 nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
885 #x; nnormalize; nelim x;
886 ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
887 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
891 nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
892 #x; nnormalize; nelim x;
893 ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
894 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
898 nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
899 #x; nnormalize; nelim x;
900 ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
901 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
905 nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
906 #x; nnormalize; nelim x;
907 ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
908 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
912 nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
913 #x; nnormalize; nelim x;
914 ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
915 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
919 nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
920 #x; nnormalize; nelim x;
921 ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
922 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
926 nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
927 #x; nnormalize; nelim x;
928 ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
929 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
933 nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
934 #x; nnormalize; nelim x;
935 ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
936 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
940 nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
941 #x; nnormalize; nelim x;
942 ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
943 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
947 nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
948 #x; nnormalize; nelim x;
949 ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
950 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
954 nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
955 #x; nnormalize; nelim x;
956 ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
957 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
961 nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
962 #x; nnormalize; nelim x;
963 ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
964 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
968 nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
969 #x; nnormalize; nelim x;
970 ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
971 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
975 nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
976 #x; nnormalize; nelim x;
977 ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
978 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
982 nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
983 #x; nnormalize; nelim x;
984 ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
985 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
989 nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
990 #x; nnormalize; nelim x;
991 ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
992 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
996 nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
997 #x; nnormalize; nelim x;
998 ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
999 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1003 nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
1004 #x; nnormalize; nelim x;
1005 ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
1006 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1010 nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
1011 #x; nnormalize; nelim x;
1012 ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
1013 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1017 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
1018 #x; nnormalize; nelim x;
1019 ##[ ##1: napply decidable_bit1 ##| ##2: napply decidable_bit2
1020 ##| ##3: napply decidable_bit3 ##| ##4: napply decidable_bit4
1021 ##| ##5: napply decidable_bit5 ##| ##6: napply decidable_bit6
1022 ##| ##7: napply decidable_bit7 ##| ##8: napply decidable_bit8
1023 ##| ##9: napply decidable_bit9 ##| ##10: napply decidable_bit10
1024 ##| ##11: napply decidable_bit11 ##| ##12: napply decidable_bit12
1025 ##| ##13: napply decidable_bit13 ##| ##14: napply decidable_bit14
1026 ##| ##15: napply decidable_bit15 ##| ##16: napply decidable_bit16
1027 ##| ##17: napply decidable_bit17 ##| ##18: napply decidable_bit18
1028 ##| ##19: napply decidable_bit19 ##| ##20: napply decidable_bit20
1029 ##| ##21: napply decidable_bit21 ##| ##22: napply decidable_bit22
1030 ##| ##23: napply decidable_bit23 ##| ##24: napply decidable_bit24
1031 ##| ##25: napply decidable_bit25 ##| ##26: napply decidable_bit26
1032 ##| ##27: napply decidable_bit27 ##| ##28: napply decidable_bit28
1033 ##| ##29: napply decidable_bit29 ##| ##30: napply decidable_bit30
1034 ##| ##31: napply decidable_bit31 ##| ##32: napply decidable_bit32
1038 nlemma neqbit_to_neq1 : ∀t2.eq_bit t00 t2 = false → t00 ≠ t2.
1039 #t2; ncases t2; nnormalize; #H;
1040 ##[ ##1: napply (bool_destruct … H)
1041 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1045 nlemma neqbit_to_neq2 : ∀t2.eq_bit t01 t2 = false → t01 ≠ t2.
1046 #t2; ncases t2; nnormalize; #H;
1047 ##[ ##2: napply (bool_destruct … H)
1048 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1052 nlemma neqbit_to_neq3 : ∀t2.eq_bit t02 t2 = false → t02 ≠ t2.
1053 #t2; ncases t2; nnormalize; #H;
1054 ##[ ##3: napply (bool_destruct … H)
1055 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1059 nlemma neqbit_to_neq4 : ∀t2.eq_bit t03 t2 = false → t03 ≠ t2.
1060 #t2; ncases t2; nnormalize; #H;
1061 ##[ ##4: napply (bool_destruct … H)
1062 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1066 nlemma neqbit_to_neq5 : ∀t2.eq_bit t04 t2 = false → t04 ≠ t2.
1067 #t2; ncases t2; nnormalize; #H;
1068 ##[ ##5: napply (bool_destruct … H)
1069 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1073 nlemma neqbit_to_neq6 : ∀t2.eq_bit t05 t2 = false → t05 ≠ t2.
1074 #t2; ncases t2; nnormalize; #H;
1075 ##[ ##6: napply (bool_destruct … H)
1076 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1080 nlemma neqbit_to_neq7 : ∀t2.eq_bit t06 t2 = false → t06 ≠ t2.
1081 #t2; ncases t2; nnormalize; #H;
1082 ##[ ##7: napply (bool_destruct … H)
1083 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1087 nlemma neqbit_to_neq8 : ∀t2.eq_bit t07 t2 = false → t07 ≠ t2.
1088 #t2; ncases t2; nnormalize; #H;
1089 ##[ ##8: napply (bool_destruct … H)
1090 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1094 nlemma neqbit_to_neq9 : ∀t2.eq_bit t08 t2 = false → t08 ≠ t2.
1095 #t2; ncases t2; nnormalize; #H;
1096 ##[ ##9: napply (bool_destruct … H)
1097 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1101 nlemma neqbit_to_neq10 : ∀t2.eq_bit t09 t2 = false → t09 ≠ t2.
1102 #t2; ncases t2; nnormalize; #H;
1103 ##[ ##10: napply (bool_destruct … H)
1104 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1108 nlemma neqbit_to_neq11 : ∀t2.eq_bit t0A t2 = false → t0A ≠ t2.
1109 #t2; ncases t2; nnormalize; #H;
1110 ##[ ##11: napply (bool_destruct … H)
1111 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1115 nlemma neqbit_to_neq12 : ∀t2.eq_bit t0B t2 = false → t0B ≠ t2.
1116 #t2; ncases t2; nnormalize; #H;
1117 ##[ ##12: napply (bool_destruct … H)
1118 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1122 nlemma neqbit_to_neq13 : ∀t2.eq_bit t0C t2 = false → t0C ≠ t2.
1123 #t2; ncases t2; nnormalize; #H;
1124 ##[ ##13: napply (bool_destruct … H)
1125 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1129 nlemma neqbit_to_neq14 : ∀t2.eq_bit t0D t2 = false → t0D ≠ t2.
1130 #t2; ncases t2; nnormalize; #H;
1131 ##[ ##14: napply (bool_destruct … H)
1132 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1136 nlemma neqbit_to_neq15 : ∀t2.eq_bit t0E t2 = false → t0E ≠ t2.
1137 #t2; ncases t2; nnormalize; #H;
1138 ##[ ##15: napply (bool_destruct … H)
1139 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1143 nlemma neqbit_to_neq16 : ∀t2.eq_bit t0F t2 = false → t0F ≠ t2.
1144 #t2; ncases t2; nnormalize; #H;
1145 ##[ ##16: napply (bool_destruct … H)
1146 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1150 nlemma neqbit_to_neq17 : ∀t2.eq_bit t10 t2 = false → t10 ≠ t2.
1151 #t2; ncases t2; nnormalize; #H;
1152 ##[ ##17: napply (bool_destruct … H)
1153 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1157 nlemma neqbit_to_neq18 : ∀t2.eq_bit t11 t2 = false → t11 ≠ t2.
1158 #t2; ncases t2; nnormalize; #H;
1159 ##[ ##18: napply (bool_destruct … H)
1160 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1164 nlemma neqbit_to_neq19 : ∀t2.eq_bit t12 t2 = false → t12 ≠ t2.
1165 #t2; ncases t2; nnormalize; #H;
1166 ##[ ##19: napply (bool_destruct … H)
1167 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1171 nlemma neqbit_to_neq20 : ∀t2.eq_bit t13 t2 = false → t13 ≠ t2.
1172 #t2; ncases t2; nnormalize; #H;
1173 ##[ ##20: napply (bool_destruct … H)
1174 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1178 nlemma neqbit_to_neq21 : ∀t2.eq_bit t14 t2 = false → t14 ≠ t2.
1179 #t2; ncases t2; nnormalize; #H;
1180 ##[ ##21: napply (bool_destruct … H)
1181 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1185 nlemma neqbit_to_neq22 : ∀t2.eq_bit t15 t2 = false → t15 ≠ t2.
1186 #t2; ncases t2; nnormalize; #H;
1187 ##[ ##22: napply (bool_destruct … H)
1188 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1192 nlemma neqbit_to_neq23 : ∀t2.eq_bit t16 t2 = false → t16 ≠ t2.
1193 #t2; ncases t2; nnormalize; #H;
1194 ##[ ##23: napply (bool_destruct … H)
1195 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1199 nlemma neqbit_to_neq24 : ∀t2.eq_bit t17 t2 = false → t17 ≠ t2.
1200 #t2; ncases t2; nnormalize; #H;
1201 ##[ ##24: napply (bool_destruct … H)
1202 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1206 nlemma neqbit_to_neq25 : ∀t2.eq_bit t18 t2 = false → t18 ≠ t2.
1207 #t2; ncases t2; nnormalize; #H;
1208 ##[ ##25: napply (bool_destruct … H)
1209 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1213 nlemma neqbit_to_neq26 : ∀t2.eq_bit t19 t2 = false → t19 ≠ t2.
1214 #t2; ncases t2; nnormalize; #H;
1215 ##[ ##26: napply (bool_destruct … H)
1216 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1220 nlemma neqbit_to_neq27 : ∀t2.eq_bit t1A t2 = false → t1A ≠ t2.
1221 #t2; ncases t2; nnormalize; #H;
1222 ##[ ##27: napply (bool_destruct … H)
1223 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1227 nlemma neqbit_to_neq28 : ∀t2.eq_bit t1B t2 = false → t1B ≠ t2.
1228 #t2; ncases t2; nnormalize; #H;
1229 ##[ ##28: napply (bool_destruct … H)
1230 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1234 nlemma neqbit_to_neq29 : ∀t2.eq_bit t1C t2 = false → t1C ≠ t2.
1235 #t2; ncases t2; nnormalize; #H;
1236 ##[ ##29: napply (bool_destruct … H)
1237 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1241 nlemma neqbit_to_neq30 : ∀t2.eq_bit t1D t2 = false → t1D ≠ t2.
1242 #t2; ncases t2; nnormalize; #H;
1243 ##[ ##30: napply (bool_destruct … H)
1244 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1248 nlemma neqbit_to_neq31 : ∀t2.eq_bit t1E t2 = false → t1E ≠ t2.
1249 #t2; ncases t2; nnormalize; #H;
1250 ##[ ##31: napply (bool_destruct … H)
1251 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1255 nlemma neqbit_to_neq32 : ∀t2.eq_bit t1F t2 = false → t1F ≠ t2.
1256 #t2; ncases t2; nnormalize; #H;
1257 ##[ ##32: napply (bool_destruct … H)
1258 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1262 nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
1264 ##[ ##1: napply neqbit_to_neq1 ##| ##2: napply neqbit_to_neq2
1265 ##| ##3: napply neqbit_to_neq3 ##| ##4: napply neqbit_to_neq4
1266 ##| ##5: napply neqbit_to_neq5 ##| ##6: napply neqbit_to_neq6
1267 ##| ##7: napply neqbit_to_neq7 ##| ##8: napply neqbit_to_neq8
1268 ##| ##9: napply neqbit_to_neq9 ##| ##10: napply neqbit_to_neq10
1269 ##| ##11: napply neqbit_to_neq11 ##| ##12: napply neqbit_to_neq12
1270 ##| ##13: napply neqbit_to_neq13 ##| ##14: napply neqbit_to_neq14
1271 ##| ##15: napply neqbit_to_neq15 ##| ##16: napply neqbit_to_neq16
1272 ##| ##17: napply neqbit_to_neq17 ##| ##18: napply neqbit_to_neq18
1273 ##| ##19: napply neqbit_to_neq19 ##| ##20: napply neqbit_to_neq20
1274 ##| ##21: napply neqbit_to_neq21 ##| ##22: napply neqbit_to_neq22
1275 ##| ##23: napply neqbit_to_neq23 ##| ##24: napply neqbit_to_neq24
1276 ##| ##25: napply neqbit_to_neq25 ##| ##26: napply neqbit_to_neq26
1277 ##| ##27: napply neqbit_to_neq27 ##| ##28: napply neqbit_to_neq28
1278 ##| ##29: napply neqbit_to_neq29 ##| ##30: napply neqbit_to_neq30
1279 ##| ##31: napply neqbit_to_neq31 ##| ##32: napply neqbit_to_neq32
1283 nlemma neq_to_neqbit1 : ∀t2.t00 ≠ t2 → eq_bit t00 t2 = false.
1284 #t2; ncases t2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1287 nlemma neq_to_neqbit2 : ∀t2.t01 ≠ t2 → eq_bit t01 t2 = false.
1288 #t2; ncases t2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1291 nlemma neq_to_neqbit3 : ∀t2.t02 ≠ t2 → eq_bit t02 t2 = false.
1292 #t2; ncases t2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1295 nlemma neq_to_neqbit4 : ∀t2.t03 ≠ t2 → eq_bit t03 t2 = false.
1296 #t2; ncases t2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1299 nlemma neq_to_neqbit5 : ∀t2.t04 ≠ t2 → eq_bit t04 t2 = false.
1300 #t2; ncases t2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1303 nlemma neq_to_neqbit6 : ∀t2.t05 ≠ t2 → eq_bit t05 t2 = false.
1304 #t2; ncases t2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1307 nlemma neq_to_neqbit7 : ∀t2.t06 ≠ t2 → eq_bit t06 t2 = false.
1308 #t2; ncases t2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1311 nlemma neq_to_neqbit8 : ∀t2.t07 ≠ t2 → eq_bit t07 t2 = false.
1312 #t2; ncases t2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1315 nlemma neq_to_neqbit9 : ∀t2.t08 ≠ t2 → eq_bit t08 t2 = false.
1316 #t2; ncases t2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1319 nlemma neq_to_neqbit10 : ∀t2.t09 ≠ t2 → eq_bit t09 t2 = false.
1320 #t2; ncases t2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1323 nlemma neq_to_neqbit11 : ∀t2.t0A ≠ t2 → eq_bit t0A t2 = false.
1324 #t2; ncases t2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1327 nlemma neq_to_neqbit12 : ∀t2.t0B ≠ t2 → eq_bit t0B t2 = false.
1328 #t2; ncases t2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1331 nlemma neq_to_neqbit13 : ∀t2.t0C ≠ t2 → eq_bit t0C t2 = false.
1332 #t2; ncases t2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1335 nlemma neq_to_neqbit14 : ∀t2.t0D ≠ t2 → eq_bit t0D t2 = false.
1336 #t2; ncases t2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1339 nlemma neq_to_neqbit15 : ∀t2.t0E ≠ t2 → eq_bit t0E t2 = false.
1340 #t2; ncases t2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1343 nlemma neq_to_neqbit16 : ∀t2.t0F ≠ t2 → eq_bit t0F t2 = false.
1344 #t2; ncases t2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1347 nlemma neq_to_neqbit17 : ∀t2.t10 ≠ t2 → eq_bit t10 t2 = false.
1348 #t2; ncases t2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1351 nlemma neq_to_neqbit18 : ∀t2.t11 ≠ t2 → eq_bit t11 t2 = false.
1352 #t2; ncases t2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1355 nlemma neq_to_neqbit19 : ∀t2.t12 ≠ t2 → eq_bit t12 t2 = false.
1356 #t2; ncases t2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1359 nlemma neq_to_neqbit20 : ∀t2.t13 ≠ t2 → eq_bit t13 t2 = false.
1360 #t2; ncases t2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1363 nlemma neq_to_neqbit21 : ∀t2.t14 ≠ t2 → eq_bit t14 t2 = false.
1364 #t2; ncases t2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1367 nlemma neq_to_neqbit22 : ∀t2.t15 ≠ t2 → eq_bit t15 t2 = false.
1368 #t2; ncases t2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1371 nlemma neq_to_neqbit23 : ∀t2.t16 ≠ t2 → eq_bit t16 t2 = false.
1372 #t2; ncases t2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1375 nlemma neq_to_neqbit24 : ∀t2.t17 ≠ t2 → eq_bit t17 t2 = false.
1376 #t2; ncases t2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1379 nlemma neq_to_neqbit25 : ∀t2.t18 ≠ t2 → eq_bit t18 t2 = false.
1380 #t2; ncases t2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1383 nlemma neq_to_neqbit26 : ∀t2.t19 ≠ t2 → eq_bit t19 t2 = false.
1384 #t2; ncases t2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1387 nlemma neq_to_neqbit27 : ∀t2.t1A ≠ t2 → eq_bit t1A t2 = false.
1388 #t2; ncases t2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1391 nlemma neq_to_neqbit28 : ∀t2.t1B ≠ t2 → eq_bit t1B t2 = false.
1392 #t2; ncases t2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1395 nlemma neq_to_neqbit29 : ∀t2.t1C ≠ t2 → eq_bit t1C t2 = false.
1396 #t2; ncases t2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1399 nlemma neq_to_neqbit30 : ∀t2.t1D ≠ t2 → eq_bit t1D t2 = false.
1400 #t2; ncases t2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1403 nlemma neq_to_neqbit31 : ∀t2.t1E ≠ t2 → eq_bit t1E t2 = false.
1404 #t2; ncases t2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1407 nlemma neq_to_neqbit32 : ∀t2.t1F ≠ t2 → eq_bit t1F t2 = false.
1408 #t2; ncases t2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1411 nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
1413 ##[ ##1: napply neq_to_neqbit1 ##| ##2: napply neq_to_neqbit2
1414 ##| ##3: napply neq_to_neqbit3 ##| ##4: napply neq_to_neqbit4
1415 ##| ##5: napply neq_to_neqbit5 ##| ##6: napply neq_to_neqbit6
1416 ##| ##7: napply neq_to_neqbit7 ##| ##8: napply neq_to_neqbit8
1417 ##| ##9: napply neq_to_neqbit9 ##| ##10: napply neq_to_neqbit10
1418 ##| ##11: napply neq_to_neqbit11 ##| ##12: napply neq_to_neqbit12
1419 ##| ##13: napply neq_to_neqbit13 ##| ##14: napply neq_to_neqbit14
1420 ##| ##15: napply neq_to_neqbit15 ##| ##16: napply neq_to_neqbit16
1421 ##| ##17: napply neq_to_neqbit17 ##| ##18: napply neq_to_neqbit18
1422 ##| ##19: napply neq_to_neqbit19 ##| ##20: napply neq_to_neqbit20
1423 ##| ##21: napply neq_to_neqbit21 ##| ##22: napply neq_to_neqbit22
1424 ##| ##23: napply neq_to_neqbit23 ##| ##24: napply neq_to_neqbit24
1425 ##| ##25: napply neq_to_neqbit25 ##| ##26: napply neq_to_neqbit26
1426 ##| ##27: napply neq_to_neqbit27 ##| ##28: napply neq_to_neqbit28
1427 ##| ##29: napply neq_to_neqbit29 ##| ##30: napply neq_to_neqbit30
1428 ##| ##31: napply neq_to_neqbit31 ##| ##32: napply neq_to_neqbit32