helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/bitrigesim.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************* *)
  27 (* BITRIGESIMALI *)
  28 (* ************* *)
  29
  30 ndefinition bitrigesim_destruct1 :
  31 Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
  32  #t2; #P;
  33  ncases t2;
  34  nnormalize; #H;
  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
  39  ##]
  40 nqed.
  41
  42 ndefinition bitrigesim_destruct2 :
  43 Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
  44  #t2; #P;
  45  ncases t2;
  46  nnormalize; #H;
  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
  51  ##]
  52 nqed.
  53
  54 ndefinition bitrigesim_destruct3 :
  55 Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
  56  #t2; #P;
  57  ncases t2;
  58  nnormalize; #H;
  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
  63  ##]
  64 nqed.
  65
  66 ndefinition bitrigesim_destruct4 :
  67 Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
  68  #t2; #P;
  69  ncases t2;
  70  nnormalize; #H;
  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
  75  ##]
  76 nqed.
  77
  78 ndefinition bitrigesim_destruct5 :
  79 Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
  80  #t2; #P;
  81  ncases t2;
  82  nnormalize; #H;
  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
  87  ##]
  88 nqed.
  89
  90 ndefinition bitrigesim_destruct6 :
  91 Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
  92  #t2; #P;
  93  ncases t2;
  94  nnormalize; #H;
  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
  99  ##]
 100 nqed.
 101
 102 ndefinition bitrigesim_destruct7 :
 103 Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
 104  #t2; #P;
 105  ncases t2;
 106  nnormalize; #H;
 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
 111  ##]
 112 nqed.
 113
 114 ndefinition bitrigesim_destruct8 :
 115 Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
 116  #t2; #P;
 117  ncases t2;
 118  nnormalize; #H;
 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
 123  ##]
 124 nqed.
 125
 126 ndefinition bitrigesim_destruct9 :
 127 Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
 128  #t2; #P;
 129  ncases t2;
 130  nnormalize; #H;
 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
 135  ##]
 136 nqed.
 137
 138 ndefinition bitrigesim_destruct10 :
 139 Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
 140  #t2; #P;
 141  ncases t2;
 142  nnormalize; #H;
 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
 147  ##]
 148 nqed.
 149
 150 ndefinition bitrigesim_destruct11 :
 151 Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
 152  #t2; #P;
 153  ncases t2;
 154  nnormalize; #H;
 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
 159  ##]
 160 nqed.
 161
 162 ndefinition bitrigesim_destruct12 :
 163 Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
 164  #t2; #P;
 165  ncases t2;
 166  nnormalize; #H;
 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
 171  ##]
 172 nqed.
 173
 174 ndefinition bitrigesim_destruct13 :
 175 Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
 176  #t2; #P;
 177  ncases t2;
 178  nnormalize; #H;
 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
 183  ##]
 184 nqed.
 185
 186 ndefinition bitrigesim_destruct14 :
 187 Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
 188  #t2; #P;
 189  ncases t2;
 190  nnormalize; #H;
 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
 195  ##]
 196 nqed.
 197
 198 ndefinition bitrigesim_destruct15 :
 199 Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
 200  #t2; #P;
 201  ncases t2;
 202  nnormalize; #H;
 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
 207  ##]
 208 nqed.
 209
 210 ndefinition bitrigesim_destruct16 :
 211 Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
 212  #t2; #P;
 213  ncases t2;
 214  nnormalize; #H;
 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
 219  ##]
 220 nqed.
 221
 222 ndefinition bitrigesim_destruct17 :
 223 Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
 224  #t2; #P;
 225  ncases t2;
 226  nnormalize; #H;
 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
 231  ##]
 232 nqed.
 233
 234 ndefinition bitrigesim_destruct18 :
 235 Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
 236  #t2; #P;
 237  ncases t2;
 238  nnormalize; #H;
 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
 243  ##]
 244 nqed.
 245
 246 ndefinition bitrigesim_destruct19 :
 247 Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
 248  #t2; #P;
 249  ncases t2;
 250  nnormalize; #H;
 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
 255  ##]
 256 nqed.
 257
 258 ndefinition bitrigesim_destruct20 :
 259 Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
 260  #t2; #P;
 261  ncases t2;
 262  nnormalize; #H;
 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
 267  ##]
 268 nqed.
 269
 270 ndefinition bitrigesim_destruct21 :
 271 Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
 272  #t2; #P;
 273  ncases t2;
 274  nnormalize; #H;
 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
 279  ##]
 280 nqed.
 281
 282 ndefinition bitrigesim_destruct22 :
 283 Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
 284  #t2; #P;
 285  ncases t2;
 286  nnormalize; #H;
 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
 291  ##]
 292 nqed.
 293
 294 ndefinition bitrigesim_destruct23 :
 295 Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
 296  #t2; #P;
 297  ncases t2;
 298  nnormalize; #H;
 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
 303  ##]
 304 nqed.
 305
 306 ndefinition bitrigesim_destruct24 :
 307 Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
 308  #t2; #P;
 309  ncases t2;
 310  nnormalize; #H;
 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
 315  ##]
 316 nqed.
 317
 318 ndefinition bitrigesim_destruct25 :
 319 Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
 320  #t2; #P;
 321  ncases t2;
 322  nnormalize; #H;
 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
 327  ##]
 328 nqed.
 329
 330 ndefinition bitrigesim_destruct26 :
 331 Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
 332  #t2; #P;
 333  ncases t2;
 334  nnormalize; #H;
 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
 339  ##]
 340 nqed.
 341
 342 ndefinition bitrigesim_destruct27 :
 343 Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
 344  #t2; #P;
 345  ncases t2;
 346  nnormalize; #H;
 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
 351  ##]
 352 nqed.
 353
 354 ndefinition bitrigesim_destruct28 :
 355 Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
 356  #t2; #P;
 357  ncases t2;
 358  nnormalize; #H;
 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
 363  ##]
 364 nqed.
 365
 366 ndefinition bitrigesim_destruct29 :
 367 Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
 368  #t2; #P;
 369  ncases t2;
 370  nnormalize; #H;
 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
 375  ##]
 376 nqed.
 377
 378 ndefinition bitrigesim_destruct30 :
 379 Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
 380  #t2; #P;
 381  ncases t2;
 382  nnormalize; #H;
 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
 387  ##]
 388 nqed.
 389
 390 ndefinition bitrigesim_destruct31 :
 391 Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
 392  #t2; #P;
 393  ncases t2;
 394  nnormalize; #H;
 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
 399  ##]
 400 nqed.
 401
 402 ndefinition bitrigesim_destruct32 :
 403 Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
 404  #t2; #P;
 405  ncases t2;
 406  nnormalize; #H;
 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
 411  ##]
 412 nqed.
 413
 414 ndefinition bitrigesim_destruct_aux ≝
 415 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
 416  match t1 with
 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 ]
 433   ].
 434
 435 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
 436  #t1;
 437  ncases t1;
 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
 454  ##]
 455 nqed.
 456
 457 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
 458  #t1;
 459  nelim t1;
 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
 492  ##]
 493 nqed.
 494
 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) ##]
 497 nqed.
 498
 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) ##]
 501 nqed.
 502
 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) ##]
 505 nqed.
 506
 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) ##]
 509 nqed.
 510
 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) ##]
 513 nqed.
 514
 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) ##]
 517 nqed.
 518
 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) ##]
 521 nqed.
 522
 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) ##]
 525 nqed.
 526
 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) ##]
 529 nqed.
 530
 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) ##]
 533 nqed.
 534
 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) ##]
 537 nqed.
 538
 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) ##]
 541 nqed.
 542
 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) ##]
 545 nqed.
 546
 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) ##]
 549 nqed.
 550
 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) ##]
 553 nqed.
 554
 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) ##]
 557 nqed.
 558
 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) ##]
 561 nqed.
 562
 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) ##]
 565 nqed.
 566
 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) ##]
 569 nqed.
 570
 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) ##]
 573 nqed.
 574
 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) ##]
 577 nqed.
 578
 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) ##]
 581 nqed.
 582
 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) ##]
 585 nqed.
 586
 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) ##]
 589 nqed.
 590
 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) ##]
 593 nqed.
 594
 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) ##]
 597 nqed.
 598
 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) ##]
 601 nqed.
 602
 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) ##]
 605 nqed.
 606
 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) ##]
 609 nqed.
 610
 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) ##]
 613 nqed.
 614
 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) ##]
 617 nqed.
 618
 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) ##]
 621 nqed.
 622
 623 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
 624  #t1; ncases t1;
 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
 641  ##]
 642 nqed.
 643
 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) ##]
 646 nqed.
 647
 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) ##]
 650 nqed.
 651
 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) ##]
 654 nqed.
 655
 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) ##]
 658 nqed.
 659
 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) ##]
 662 nqed.
 663
 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) ##]
 666 nqed.
 667
 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) ##]
 670 nqed.
 671
 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) ##]
 674 nqed.
 675
 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) ##]
 678 nqed.
 679
 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) ##]
 682 nqed.
 683
 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) ##]
 686 nqed.
 687
 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) ##]
 690 nqed.
 691
 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) ##]
 694 nqed.
 695
 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) ##]
 698 nqed.
 699
 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) ##]
 702 nqed.
 703
 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) ##]
 706 nqed.
 707
 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) ##]
 710 nqed.
 711
 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) ##]
 714 nqed.
 715
 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) ##]
 718 nqed.
 719
 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) ##]
 722 nqed.
 723
 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) ##]
 726 nqed.
 727
 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) ##]
 730 nqed.
 731
 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) ##]
 734 nqed.
 735
 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) ##]
 738 nqed.
 739
 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) ##]
 742 nqed.
 743
 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) ##]
 746 nqed.
 747
 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) ##]
 750 nqed.
 751
 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) ##]
 754 nqed.
 755
 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) ##]
 758 nqed.
 759
 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) ##]
 762 nqed.
 763
 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) ##]
 766 nqed.
 767
 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) ##]
 770 nqed.
 771
 772 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
 773  #t1; ncases t1;
 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
 790  ##]
 791 nqed.
 792
 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)
 797  ##]
 798 nqed.
 799
 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)
 804  ##]
 805 nqed.
 806
 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)
 811  ##]
 812 nqed.
 813
 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)
 818  ##]
 819 nqed.
 820
 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)
 825  ##]
 826 nqed.
 827
 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)
 832  ##]
 833 nqed.
 834
 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)
 839  ##]
 840 nqed.
 841
 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)
 846  ##]
 847 nqed.
 848
 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)
 853  ##]
 854 nqed.
 855
 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)
 860  ##]
 861 nqed.
 862
 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)
 867  ##]
 868 nqed.
 869
 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)
 874  ##]
 875 nqed.
 876
 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)
 881  ##]
 882 nqed.
 883
 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)
 888  ##]
 889 nqed.
 890
 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)
 895  ##]
 896 nqed.
 897
 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)
 902  ##]
 903 nqed.
 904
 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)
 909  ##]
 910 nqed.
 911
 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)
 916  ##]
 917 nqed.
 918
 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)
 923  ##]
 924 nqed.
 925
 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)
 930  ##]
 931 nqed.
 932
 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)
 937  ##]
 938 nqed.
 939
 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)
 944  ##]
 945 nqed.
 946
 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)
 951  ##]
 952 nqed.
 953
 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)
 958  ##]
 959 nqed.
 960
 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)
 965  ##]
 966 nqed.
 967
 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)
 972  ##]
 973 nqed.
 974
 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)
 979  ##]
 980 nqed.
 981
 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)
 986  ##]
 987 nqed.
 988
 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)
 993  ##]
 994 nqed.
 995
 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)
1000  ##]
1001 nqed.
1002
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)
1007  ##]
1008 nqed.
1009
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)
1014  ##]
1015 nqed.
1016
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
1035  ##]
1036 nqed.
1037
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)
1042  ##]
1043 nqed.
1044
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)
1049  ##]
1050 nqed.
1051
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)
1056  ##]
1057 nqed.
1058
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)
1063  ##]
1064 nqed.
1065
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)
1070  ##]
1071 nqed.
1072
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)
1077  ##]
1078 nqed.
1079
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)
1084  ##]
1085 nqed.
1086
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)
1091  ##]
1092 nqed.
1093
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)
1098  ##]
1099 nqed.
1100
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)
1105  ##]
1106 nqed.
1107
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)
1112  ##]
1113 nqed.
1114
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)
1119  ##]
1120 nqed.
1121
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)
1126  ##]
1127 nqed.
1128
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)
1133  ##]
1134 nqed.
1135
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)
1140  ##]
1141 nqed.
1142
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)
1147  ##]
1148 nqed.
1149
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)
1154  ##]
1155 nqed.
1156
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)
1161  ##]
1162 nqed.
1163
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)
1168  ##]
1169 nqed.
1170
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)
1175  ##]
1176 nqed.
1177
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)
1182  ##]
1183 nqed.
1184
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)
1189  ##]
1190 nqed.
1191
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)
1196  ##]
1197 nqed.
1198
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)
1203  ##]
1204 nqed.
1205
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)
1210  ##]
1211 nqed.
1212
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)
1217  ##]
1218 nqed.
1219
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)
1224  ##]
1225 nqed.
1226
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)
1231  ##]
1232 nqed.
1233
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)
1238  ##]
1239 nqed.
1240
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)
1245  ##]
1246 nqed.
1247
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)
1252  ##]
1253 nqed.
1254
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)
1259  ##]
1260 nqed.
1261
1262 nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
1263  #t1; nelim t1;
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
1280  ##]
1281 nqed.
1282
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 ##]
1285 nqed.
1286
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 ##]
1289 nqed.
1290
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 ##]
1293 nqed.
1294
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 ##]
1297 nqed.
1298
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 ##]
1301 nqed.
1302
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 ##]
1305 nqed.
1306
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 ##]
1309 nqed.
1310
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 ##]
1313 nqed.
1314
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 ##]
1317 nqed.
1318
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 ##]
1321 nqed.
1322
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 ##]
1325 nqed.
1326
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 ##]
1329 nqed.
1330
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 ##]
1333 nqed.
1334
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 ##]
1337 nqed.
1338
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 ##]
1341 nqed.
1342
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 ##]
1345 nqed.
1346
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 ##]
1349 nqed.
1350
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 ##]
1353 nqed.
1354
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 ##]
1357 nqed.
1358
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 ##]
1361 nqed.
1362
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 ##]
1365 nqed.
1366
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 ##]
1369 nqed.
1370
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 ##]
1373 nqed.
1374
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 ##]
1377 nqed.
1378
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 ##]
1381 nqed.
1382
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 ##]
1385 nqed.
1386
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 ##]
1389 nqed.
1390
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 ##]
1393 nqed.
1394
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 ##]
1397 nqed.
1398
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 ##]
1401 nqed.
1402
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 ##]
1405 nqed.
1406
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 ##]
1409 nqed.
1410
1411 nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
1412  #t1; nelim t1;
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
1429  ##]
1430 nqed.