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 ]
 418   | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
 419   | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
 420   | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
 421   | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
 422   | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
 423   | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
 424   | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
 425   | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
 426   | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
 427   | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
 428   | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
 429   | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
 430   | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
 431   | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
 432   | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
 433   | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
 434   | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
 435   | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
 436   | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
 437   | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
 438   | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
 439   | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
 440   | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
 441   | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
 442   | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
 443   | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
 444   | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
 445   | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
 446   | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
 447   | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
 448   | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
 449   ].
 450
 451 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
 452  #t1;
 453  ncases t1;
 454  ##[ ##1: napply bitrigesim_destruct1
 455  ##| ##2: napply bitrigesim_destruct2
 456  ##| ##3: napply bitrigesim_destruct3
 457  ##| ##4: napply bitrigesim_destruct4
 458  ##| ##5: napply bitrigesim_destruct5
 459  ##| ##6: napply bitrigesim_destruct6
 460  ##| ##7: napply bitrigesim_destruct7
 461  ##| ##8: napply bitrigesim_destruct8
 462  ##| ##9: napply bitrigesim_destruct9
 463  ##| ##10: napply bitrigesim_destruct10
 464  ##| ##11: napply bitrigesim_destruct11
 465  ##| ##12: napply bitrigesim_destruct12
 466  ##| ##13: napply bitrigesim_destruct13
 467  ##| ##14: napply bitrigesim_destruct14
 468  ##| ##15: napply bitrigesim_destruct15
 469  ##| ##16: napply bitrigesim_destruct16
 470  ##| ##17: napply bitrigesim_destruct17
 471  ##| ##18: napply bitrigesim_destruct18
 472  ##| ##19: napply bitrigesim_destruct19
 473  ##| ##20: napply bitrigesim_destruct20
 474  ##| ##21: napply bitrigesim_destruct21
 475  ##| ##22: napply bitrigesim_destruct22
 476  ##| ##23: napply bitrigesim_destruct23
 477  ##| ##24: napply bitrigesim_destruct24
 478  ##| ##25: napply bitrigesim_destruct25
 479  ##| ##26: napply bitrigesim_destruct26
 480  ##| ##27: napply bitrigesim_destruct27
 481  ##| ##28: napply bitrigesim_destruct28
 482  ##| ##29: napply bitrigesim_destruct29
 483  ##| ##30: napply bitrigesim_destruct30
 484  ##| ##31: napply bitrigesim_destruct31
 485  ##| ##32: napply bitrigesim_destruct32
 486  ##]
 487 nqed.
 488
 489 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
 490  #t1;
 491  nelim t1;
 492  ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
 493  ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
 494  ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
 495  ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
 496  ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
 497  ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
 498  ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
 499  ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
 500  ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
 501  ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
 502  ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
 503  ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
 504  ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
 505  ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
 506  ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
 507  ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
 508  ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
 509  ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
 510  ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
 511  ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
 512  ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
 513  ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
 514  ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
 515  ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
 516  ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
 517  ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
 518  ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
 519  ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
 520  ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
 521  ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
 522  ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
 523  ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
 524  ##]
 525 nqed.
 526
 527 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
 528  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 529 nqed.
 530
 531 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
 532  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 533 nqed.
 534
 535 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
 536  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 537 nqed.
 538
 539 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
 540  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 541 nqed.
 542
 543 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
 544  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 545 nqed.
 546
 547 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
 548  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 549 nqed.
 550
 551 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
 552  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 553 nqed.
 554
 555 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
 556  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 557 nqed.
 558
 559 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
 560  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 561 nqed.
 562
 563 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
 564  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 565 nqed.
 566
 567 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
 568  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 569 nqed.
 570
 571 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
 572  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 573 nqed.
 574
 575 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
 576  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 577 nqed.
 578
 579 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
 580  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 581 nqed.
 582
 583 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
 584  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 585 nqed.
 586
 587 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
 588  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 589 nqed.
 590
 591 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
 592  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 593 nqed.
 594
 595 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
 596  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 597 nqed.
 598
 599 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
 600  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 601 nqed.
 602
 603 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
 604  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 605 nqed.
 606
 607 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
 608  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 609 nqed.
 610
 611 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
 612  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 613 nqed.
 614
 615 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
 616  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 617 nqed.
 618
 619 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
 620  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 621 nqed.
 622
 623 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
 624  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 625 nqed.
 626
 627 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
 628  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 629 nqed.
 630
 631 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
 632  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 633 nqed.
 634
 635 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
 636  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 637 nqed.
 638
 639 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
 640  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 641 nqed.
 642
 643 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
 644  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 645 nqed.
 646
 647 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
 648  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 649 nqed.
 650
 651 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
 652  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 653 nqed.
 654
 655 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
 656  #t1;
 657  ncases t1;
 658  ##[ ##1: napply eqbit_to_eq1
 659  ##| ##2: napply eqbit_to_eq2
 660  ##| ##3: napply eqbit_to_eq3
 661  ##| ##4: napply eqbit_to_eq4
 662  ##| ##5: napply eqbit_to_eq5
 663  ##| ##6: napply eqbit_to_eq6
 664  ##| ##7: napply eqbit_to_eq7
 665  ##| ##8: napply eqbit_to_eq8
 666  ##| ##9: napply eqbit_to_eq9
 667  ##| ##10: napply eqbit_to_eq10
 668  ##| ##11: napply eqbit_to_eq11
 669  ##| ##12: napply eqbit_to_eq12
 670  ##| ##13: napply eqbit_to_eq13
 671  ##| ##14: napply eqbit_to_eq14
 672  ##| ##15: napply eqbit_to_eq15
 673  ##| ##16: napply eqbit_to_eq16
 674  ##| ##17: napply eqbit_to_eq17
 675  ##| ##18: napply eqbit_to_eq18
 676  ##| ##19: napply eqbit_to_eq19
 677  ##| ##20: napply eqbit_to_eq20
 678  ##| ##21: napply eqbit_to_eq21
 679  ##| ##22: napply eqbit_to_eq22
 680  ##| ##23: napply eqbit_to_eq23
 681  ##| ##24: napply eqbit_to_eq24
 682  ##| ##25: napply eqbit_to_eq25
 683  ##| ##26: napply eqbit_to_eq26
 684  ##| ##27: napply eqbit_to_eq27
 685  ##| ##28: napply eqbit_to_eq28
 686  ##| ##29: napply eqbit_to_eq29
 687  ##| ##30: napply eqbit_to_eq30
 688  ##| ##31: napply eqbit_to_eq31
 689  ##| ##32: napply eqbit_to_eq32
 690  ##]
 691 nqed.
 692
 693 nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
 694  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 695 nqed.
 696
 697 nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
 698  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 699 nqed.
 700
 701 nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
 702  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 703 nqed.
 704
 705 nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
 706  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 707 nqed.
 708
 709 nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
 710  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 711 nqed.
 712
 713 nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
 714  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 715 nqed.
 716
 717 nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
 718  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 719 nqed.
 720
 721 nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
 722  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 723 nqed.
 724
 725 nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
 726  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 727 nqed.
 728
 729 nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
 730  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 731 nqed.
 732
 733 nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
 734  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 735 nqed.
 736
 737 nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
 738  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 739 nqed.
 740
 741 nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
 742  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 743 nqed.
 744
 745 nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
 746  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 747 nqed.
 748
 749 nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
 750  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 751 nqed.
 752
 753 nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
 754  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 755 nqed.
 756
 757 nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
 758  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 759 nqed.
 760
 761 nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
 762  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 763 nqed.
 764
 765 nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
 766  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 767 nqed.
 768
 769 nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
 770  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 771 nqed.
 772
 773 nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
 774  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 775 nqed.
 776
 777 nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
 778  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 779 nqed.
 780
 781 nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
 782  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 783 nqed.
 784
 785 nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
 786  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 787 nqed.
 788
 789 nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
 790  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 791 nqed.
 792
 793 nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
 794  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 795 nqed.
 796
 797 nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
 798  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 799 nqed.
 800
 801 nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
 802  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 803 nqed.
 804
 805 nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
 806  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 807 nqed.
 808
 809 nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
 810  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 811 nqed.
 812
 813 nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
 814  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 815 nqed.
 816
 817 nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
 818  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 819 nqed.
 820
 821 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
 822  #t1;
 823  ncases t1;
 824  ##[ ##1: napply eq_to_eqbit1
 825  ##| ##2: napply eq_to_eqbit2
 826  ##| ##3: napply eq_to_eqbit3
 827  ##| ##4: napply eq_to_eqbit4
 828  ##| ##5: napply eq_to_eqbit5
 829  ##| ##6: napply eq_to_eqbit6
 830  ##| ##7: napply eq_to_eqbit7
 831  ##| ##8: napply eq_to_eqbit8
 832  ##| ##9: napply eq_to_eqbit9
 833  ##| ##10: napply eq_to_eqbit10
 834  ##| ##11: napply eq_to_eqbit11
 835  ##| ##12: napply eq_to_eqbit12
 836  ##| ##13: napply eq_to_eqbit13
 837  ##| ##14: napply eq_to_eqbit14
 838  ##| ##15: napply eq_to_eqbit15
 839  ##| ##16: napply eq_to_eqbit16
 840  ##| ##17: napply eq_to_eqbit17
 841  ##| ##18: napply eq_to_eqbit18
 842  ##| ##19: napply eq_to_eqbit19
 843  ##| ##20: napply eq_to_eqbit20
 844  ##| ##21: napply eq_to_eqbit21
 845  ##| ##22: napply eq_to_eqbit22
 846  ##| ##23: napply eq_to_eqbit23
 847  ##| ##24: napply eq_to_eqbit24
 848  ##| ##25: napply eq_to_eqbit25
 849  ##| ##26: napply eq_to_eqbit26
 850  ##| ##27: napply eq_to_eqbit27
 851  ##| ##28: napply eq_to_eqbit28
 852  ##| ##29: napply eq_to_eqbit29
 853  ##| ##30: napply eq_to_eqbit30
 854  ##| ##31: napply eq_to_eqbit31
 855  ##| ##32: napply eq_to_eqbit32
 856  ##]
 857 nqed.
 858
 859 nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
 860  #x; nnormalize; nelim x;
 861  ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 862  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 863  ##]
 864 nqed.
 865
 866 nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
 867  #x; nnormalize; nelim x;
 868  ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 869  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 870  ##]
 871 nqed.
 872
 873 nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
 874  #x; nnormalize; nelim x;
 875  ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 876  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 877  ##]
 878 nqed.
 879
 880 nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
 881  #x; nnormalize; nelim x;
 882  ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 883  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 884  ##]
 885 nqed.
 886
 887 nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
 888  #x; nnormalize; nelim x;
 889  ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 890  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 891  ##]
 892 nqed.
 893
 894 nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
 895  #x; nnormalize; nelim x;
 896  ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 897  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 898  ##]
 899 nqed.
 900
 901 nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
 902  #x; nnormalize; nelim x;
 903  ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 904  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 905  ##]
 906 nqed.
 907
 908 nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
 909  #x; nnormalize; nelim x;
 910  ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 911  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 912  ##]
 913 nqed.
 914
 915 nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
 916  #x; nnormalize; nelim x;
 917  ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 918  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 919  ##]
 920 nqed.
 921
 922 nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
 923  #x; nnormalize; nelim x;
 924  ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 925  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 926  ##]
 927 nqed.
 928
 929 nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
 930  #x; nnormalize; nelim x;
 931  ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 932  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 933  ##]
 934 nqed.
 935
 936 nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
 937  #x; nnormalize; nelim x;
 938  ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 939  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 940  ##]
 941 nqed.
 942
 943 nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
 944  #x; nnormalize; nelim x;
 945  ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 946  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 947  ##]
 948 nqed.
 949
 950 nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
 951  #x; nnormalize; nelim x;
 952  ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 953  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 954  ##]
 955 nqed.
 956
 957 nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
 958  #x; nnormalize; nelim x;
 959  ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 960  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 961  ##]
 962 nqed.
 963
 964 nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
 965  #x; nnormalize; nelim x;
 966  ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 967  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 968  ##]
 969 nqed.
 970
 971 nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
 972  #x; nnormalize; nelim x;
 973  ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 974  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 975  ##]
 976 nqed.
 977
 978 nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
 979  #x; nnormalize; nelim x;
 980  ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 981  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 982  ##]
 983 nqed.
 984
 985 nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
 986  #x; nnormalize; nelim x;
 987  ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 988  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 989  ##]
 990 nqed.
 991
 992 nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
 993  #x; nnormalize; nelim x;
 994  ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
 995  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 996  ##]
 997 nqed.
 998
 999 nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
1000  #x; nnormalize; nelim x;
1001  ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1002  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1003  ##]
1004 nqed.
1005
1006 nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
1007  #x; nnormalize; nelim x;
1008  ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1009  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1010  ##]
1011 nqed.
1012
1013 nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
1014  #x; nnormalize; nelim x;
1015  ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1016  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1017  ##]
1018 nqed.
1019
1020 nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
1021  #x; nnormalize; nelim x;
1022  ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1023  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1024  ##]
1025 nqed.
1026
1027 nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
1028  #x; nnormalize; nelim x;
1029  ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1030  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1031  ##]
1032 nqed.
1033
1034 nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
1035  #x; nnormalize; nelim x;
1036  ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1037  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1038  ##]
1039 nqed.
1040
1041 nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
1042  #x; nnormalize; nelim x;
1043  ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1044  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1045  ##]
1046 nqed.
1047
1048 nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
1049  #x; nnormalize; nelim x;
1050  ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1051  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1052  ##]
1053 nqed.
1054
1055 nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
1056  #x; nnormalize; nelim x;
1057  ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1058  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1059  ##]
1060 nqed.
1061
1062 nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
1063  #x; nnormalize; nelim x;
1064  ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1065  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1066  ##]
1067 nqed.
1068
1069 nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
1070  #x; nnormalize; nelim x;
1071  ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1072  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1073  ##]
1074 nqed.
1075
1076 nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
1077  #x; nnormalize; nelim x;
1078  ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
1079  ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
1080  ##]
1081 nqed.
1082
1083 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
1084  #x; nnormalize; nelim x;
1085  ##[ ##1: napply decidable_bit1
1086  ##| ##2: napply decidable_bit2
1087  ##| ##3: napply decidable_bit3
1088  ##| ##4: napply decidable_bit4
1089  ##| ##5: napply decidable_bit5
1090  ##| ##6: napply decidable_bit6
1091  ##| ##7: napply decidable_bit7
1092  ##| ##8: napply decidable_bit8
1093  ##| ##9: napply decidable_bit9
1094  ##| ##10: napply decidable_bit10
1095  ##| ##11: napply decidable_bit11
1096  ##| ##12: napply decidable_bit12
1097  ##| ##13: napply decidable_bit13
1098  ##| ##14: napply decidable_bit14
1099  ##| ##15: napply decidable_bit15
1100  ##| ##16: napply decidable_bit16
1101  ##| ##17: napply decidable_bit17
1102  ##| ##18: napply decidable_bit18
1103  ##| ##19: napply decidable_bit19
1104  ##| ##20: napply decidable_bit20
1105  ##| ##21: napply decidable_bit21
1106  ##| ##22: napply decidable_bit22
1107  ##| ##23: napply decidable_bit23
1108  ##| ##24: napply decidable_bit24
1109  ##| ##25: napply decidable_bit25
1110  ##| ##26: napply decidable_bit26
1111  ##| ##27: napply decidable_bit27
1112  ##| ##28: napply decidable_bit28
1113  ##| ##29: napply decidable_bit29
1114  ##| ##30: napply decidable_bit30
1115  ##| ##31: napply decidable_bit31
1116  ##| ##32: napply decidable_bit32
1117  ##]
1118 nqed.
1119
1120 nlemma neqbit_to_neq1 : ∀t2.eq_bit t00 t2 = false → t00 ≠ t2.
1121  #t2; ncases t2; nnormalize; #H;
1122  ##[ ##1: napply  (bool_destruct … H)
1123  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1124  ##]
1125 nqed.
1126
1127 nlemma neqbit_to_neq2 : ∀t2.eq_bit t01 t2 = false → t01 ≠ t2.
1128  #t2; ncases t2; nnormalize; #H;
1129  ##[ ##2: napply  (bool_destruct … H)
1130  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1131  ##]
1132 nqed.
1133
1134 nlemma neqbit_to_neq3 : ∀t2.eq_bit t02 t2 = false → t02 ≠ t2.
1135  #t2; ncases t2; nnormalize; #H;
1136  ##[ ##3: napply  (bool_destruct … H)
1137  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1138  ##]
1139 nqed.
1140
1141 nlemma neqbit_to_neq4 : ∀t2.eq_bit t03 t2 = false → t03 ≠ t2.
1142  #t2; ncases t2; nnormalize; #H;
1143  ##[ ##4: napply  (bool_destruct … H)
1144  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1145  ##]
1146 nqed.
1147
1148 nlemma neqbit_to_neq5 : ∀t2.eq_bit t04 t2 = false → t04 ≠ t2.
1149  #t2; ncases t2; nnormalize; #H;
1150  ##[ ##5: napply  (bool_destruct … H)
1151  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1152  ##]
1153 nqed.
1154
1155 nlemma neqbit_to_neq6 : ∀t2.eq_bit t05 t2 = false → t05 ≠ t2.
1156  #t2; ncases t2; nnormalize; #H;
1157  ##[ ##6: napply  (bool_destruct … H)
1158  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1159  ##]
1160 nqed.
1161
1162 nlemma neqbit_to_neq7 : ∀t2.eq_bit t06 t2 = false → t06 ≠ t2.
1163  #t2; ncases t2; nnormalize; #H;
1164  ##[ ##7: napply  (bool_destruct … H)
1165  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1166  ##]
1167 nqed.
1168
1169 nlemma neqbit_to_neq8 : ∀t2.eq_bit t07 t2 = false → t07 ≠ t2.
1170  #t2; ncases t2; nnormalize; #H;
1171  ##[ ##8: napply  (bool_destruct … H)
1172  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1173  ##]
1174 nqed.
1175
1176 nlemma neqbit_to_neq9 : ∀t2.eq_bit t08 t2 = false → t08 ≠ t2.
1177  #t2; ncases t2; nnormalize; #H;
1178  ##[ ##9: napply  (bool_destruct … H)
1179  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1180  ##]
1181 nqed.
1182
1183 nlemma neqbit_to_neq10 : ∀t2.eq_bit t09 t2 = false → t09 ≠ t2.
1184  #t2; ncases t2; nnormalize; #H;
1185  ##[ ##10: napply  (bool_destruct … H)
1186  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1187  ##]
1188 nqed.
1189
1190 nlemma neqbit_to_neq11 : ∀t2.eq_bit t0A t2 = false → t0A ≠ t2.
1191  #t2; ncases t2; nnormalize; #H;
1192  ##[ ##11: napply  (bool_destruct … H)
1193  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1194  ##]
1195 nqed.
1196
1197 nlemma neqbit_to_neq12 : ∀t2.eq_bit t0B t2 = false → t0B ≠ t2.
1198  #t2; ncases t2; nnormalize; #H;
1199  ##[ ##12: napply  (bool_destruct … H)
1200  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1201  ##]
1202 nqed.
1203
1204 nlemma neqbit_to_neq13 : ∀t2.eq_bit t0C t2 = false → t0C ≠ t2.
1205  #t2; ncases t2; nnormalize; #H;
1206  ##[ ##13: napply  (bool_destruct … H)
1207  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1208  ##]
1209 nqed.
1210
1211 nlemma neqbit_to_neq14 : ∀t2.eq_bit t0D t2 = false → t0D ≠ t2.
1212  #t2; ncases t2; nnormalize; #H;
1213  ##[ ##14: napply  (bool_destruct … H)
1214  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1215  ##]
1216 nqed.
1217
1218 nlemma neqbit_to_neq15 : ∀t2.eq_bit t0E t2 = false → t0E ≠ t2.
1219  #t2; ncases t2; nnormalize; #H;
1220  ##[ ##15: napply  (bool_destruct … H)
1221  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1222  ##]
1223 nqed.
1224
1225 nlemma neqbit_to_neq16 : ∀t2.eq_bit t0F t2 = false → t0F ≠ t2.
1226  #t2; ncases t2; nnormalize; #H;
1227  ##[ ##16: napply  (bool_destruct … H)
1228  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1229  ##]
1230 nqed.
1231
1232 nlemma neqbit_to_neq17 : ∀t2.eq_bit t10 t2 = false → t10 ≠ t2.
1233  #t2; ncases t2; nnormalize; #H;
1234  ##[ ##17: napply  (bool_destruct … H)
1235  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1236  ##]
1237 nqed.
1238
1239 nlemma neqbit_to_neq18 : ∀t2.eq_bit t11 t2 = false → t11 ≠ t2.
1240  #t2; ncases t2; nnormalize; #H;
1241  ##[ ##18: napply  (bool_destruct … H)
1242  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1243  ##]
1244 nqed.
1245
1246 nlemma neqbit_to_neq19 : ∀t2.eq_bit t12 t2 = false → t12 ≠ t2.
1247  #t2; ncases t2; nnormalize; #H;
1248  ##[ ##19: napply  (bool_destruct … H)
1249  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1250  ##]
1251 nqed.
1252
1253 nlemma neqbit_to_neq20 : ∀t2.eq_bit t13 t2 = false → t13 ≠ t2.
1254  #t2; ncases t2; nnormalize; #H;
1255  ##[ ##20: napply  (bool_destruct … H)
1256  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1257  ##]
1258 nqed.
1259
1260 nlemma neqbit_to_neq21 : ∀t2.eq_bit t14 t2 = false → t14 ≠ t2.
1261  #t2; ncases t2; nnormalize; #H;
1262  ##[ ##21: napply  (bool_destruct … H)
1263  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1264  ##]
1265 nqed.
1266
1267 nlemma neqbit_to_neq22 : ∀t2.eq_bit t15 t2 = false → t15 ≠ t2.
1268  #t2; ncases t2; nnormalize; #H;
1269  ##[ ##22: napply  (bool_destruct … H)
1270  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1271  ##]
1272 nqed.
1273
1274 nlemma neqbit_to_neq23 : ∀t2.eq_bit t16 t2 = false → t16 ≠ t2.
1275  #t2; ncases t2; nnormalize; #H;
1276  ##[ ##23: napply  (bool_destruct … H)
1277  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1278  ##]
1279 nqed.
1280
1281 nlemma neqbit_to_neq24 : ∀t2.eq_bit t17 t2 = false → t17 ≠ t2.
1282  #t2; ncases t2; nnormalize; #H;
1283  ##[ ##24: napply  (bool_destruct … H)
1284  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1285  ##]
1286 nqed.
1287
1288 nlemma neqbit_to_neq25 : ∀t2.eq_bit t18 t2 = false → t18 ≠ t2.
1289  #t2; ncases t2; nnormalize; #H;
1290  ##[ ##25: napply  (bool_destruct … H)
1291  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1292  ##]
1293 nqed.
1294
1295 nlemma neqbit_to_neq26 : ∀t2.eq_bit t19 t2 = false → t19 ≠ t2.
1296  #t2; ncases t2; nnormalize; #H;
1297  ##[ ##26: napply  (bool_destruct … H)
1298  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1299  ##]
1300 nqed.
1301
1302 nlemma neqbit_to_neq27 : ∀t2.eq_bit t1A t2 = false → t1A ≠ t2.
1303  #t2; ncases t2; nnormalize; #H;
1304  ##[ ##27: napply  (bool_destruct … H)
1305  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1306  ##]
1307 nqed.
1308
1309 nlemma neqbit_to_neq28 : ∀t2.eq_bit t1B t2 = false → t1B ≠ t2.
1310  #t2; ncases t2; nnormalize; #H;
1311  ##[ ##28: napply  (bool_destruct … H)
1312  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1313  ##]
1314 nqed.
1315
1316 nlemma neqbit_to_neq29 : ∀t2.eq_bit t1C t2 = false → t1C ≠ t2.
1317  #t2; ncases t2; nnormalize; #H;
1318  ##[ ##29: napply  (bool_destruct … H)
1319  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1320  ##]
1321 nqed.
1322
1323 nlemma neqbit_to_neq30 : ∀t2.eq_bit t1D t2 = false → t1D ≠ t2.
1324  #t2; ncases t2; nnormalize; #H;
1325  ##[ ##30: napply  (bool_destruct … H)
1326  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1327  ##]
1328 nqed.
1329
1330 nlemma neqbit_to_neq31 : ∀t2.eq_bit t1E t2 = false → t1E ≠ t2.
1331  #t2; ncases t2; nnormalize; #H;
1332  ##[ ##31: napply  (bool_destruct … H)
1333  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1334  ##]
1335 nqed.
1336
1337 nlemma neqbit_to_neq32 : ∀t2.eq_bit t1F t2 = false → t1F ≠ t2.
1338  #t2; ncases t2; nnormalize; #H;
1339  ##[ ##32: napply  (bool_destruct … H)
1340  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
1341  ##]
1342 nqed.
1343
1344 nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
1345  #t1; nelim t1;
1346  ##[ ##1: napply neqbit_to_neq1
1347  ##| ##2: napply neqbit_to_neq2
1348  ##| ##3: napply neqbit_to_neq3
1349  ##| ##4: napply neqbit_to_neq4
1350  ##| ##5: napply neqbit_to_neq5
1351  ##| ##6: napply neqbit_to_neq6
1352  ##| ##7: napply neqbit_to_neq7
1353  ##| ##8: napply neqbit_to_neq8
1354  ##| ##9: napply neqbit_to_neq9
1355  ##| ##10: napply neqbit_to_neq10
1356  ##| ##11: napply neqbit_to_neq11
1357  ##| ##12: napply neqbit_to_neq12
1358  ##| ##13: napply neqbit_to_neq13
1359  ##| ##14: napply neqbit_to_neq14
1360  ##| ##15: napply neqbit_to_neq15
1361  ##| ##16: napply neqbit_to_neq16
1362  ##| ##17: napply neqbit_to_neq17
1363  ##| ##18: napply neqbit_to_neq18
1364  ##| ##19: napply neqbit_to_neq19
1365  ##| ##20: napply neqbit_to_neq20
1366  ##| ##21: napply neqbit_to_neq21
1367  ##| ##22: napply neqbit_to_neq22
1368  ##| ##23: napply neqbit_to_neq23
1369  ##| ##24: napply neqbit_to_neq24
1370  ##| ##25: napply neqbit_to_neq25
1371  ##| ##26: napply neqbit_to_neq26
1372  ##| ##27: napply neqbit_to_neq27
1373  ##| ##28: napply neqbit_to_neq28
1374  ##| ##29: napply neqbit_to_neq29
1375  ##| ##30: napply neqbit_to_neq30
1376  ##| ##31: napply neqbit_to_neq31
1377  ##| ##32: napply neqbit_to_neq32
1378  ##]
1379 nqed.
1380
1381 nlemma neq_to_neqbit1 : ∀t2.t00 ≠ t2 → eq_bit t00 t2 = false.
1382  #t2; ncases t2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1383 nqed.
1384
1385 nlemma neq_to_neqbit2 : ∀t2.t01 ≠ t2 → eq_bit t01 t2 = false.
1386  #t2; ncases t2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1387 nqed.
1388
1389 nlemma neq_to_neqbit3 : ∀t2.t02 ≠ t2 → eq_bit t02 t2 = false.
1390  #t2; ncases t2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1391 nqed.
1392
1393 nlemma neq_to_neqbit4 : ∀t2.t03 ≠ t2 → eq_bit t03 t2 = false.
1394  #t2; ncases t2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1395 nqed.
1396
1397 nlemma neq_to_neqbit5 : ∀t2.t04 ≠ t2 → eq_bit t04 t2 = false.
1398  #t2; ncases t2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1399 nqed.
1400
1401 nlemma neq_to_neqbit6 : ∀t2.t05 ≠ t2 → eq_bit t05 t2 = false.
1402  #t2; ncases t2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1403 nqed.
1404
1405 nlemma neq_to_neqbit7 : ∀t2.t06 ≠ t2 → eq_bit t06 t2 = false.
1406  #t2; ncases t2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1407 nqed.
1408
1409 nlemma neq_to_neqbit8 : ∀t2.t07 ≠ t2 → eq_bit t07 t2 = false.
1410  #t2; ncases t2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1411 nqed.
1412
1413 nlemma neq_to_neqbit9 : ∀t2.t08 ≠ t2 → eq_bit t08 t2 = false.
1414  #t2; ncases t2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1415 nqed.
1416
1417 nlemma neq_to_neqbit10 : ∀t2.t09 ≠ t2 → eq_bit t09 t2 = false.
1418  #t2; ncases t2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1419 nqed.
1420
1421 nlemma neq_to_neqbit11 : ∀t2.t0A ≠ t2 → eq_bit t0A t2 = false.
1422  #t2; ncases t2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1423 nqed.
1424
1425 nlemma neq_to_neqbit12 : ∀t2.t0B ≠ t2 → eq_bit t0B t2 = false.
1426  #t2; ncases t2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1427 nqed.
1428
1429 nlemma neq_to_neqbit13 : ∀t2.t0C ≠ t2 → eq_bit t0C t2 = false.
1430  #t2; ncases t2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1431 nqed.
1432
1433 nlemma neq_to_neqbit14 : ∀t2.t0D ≠ t2 → eq_bit t0D t2 = false.
1434  #t2; ncases t2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1435 nqed.
1436
1437 nlemma neq_to_neqbit15 : ∀t2.t0E ≠ t2 → eq_bit t0E t2 = false.
1438  #t2; ncases t2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1439 nqed.
1440
1441 nlemma neq_to_neqbit16 : ∀t2.t0F ≠ t2 → eq_bit t0F t2 = false.
1442  #t2; ncases t2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1443 nqed.
1444
1445 nlemma neq_to_neqbit17 : ∀t2.t10 ≠ t2 → eq_bit t10 t2 = false.
1446  #t2; ncases t2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1447 nqed.
1448
1449 nlemma neq_to_neqbit18 : ∀t2.t11 ≠ t2 → eq_bit t11 t2 = false.
1450  #t2; ncases t2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1451 nqed.
1452
1453 nlemma neq_to_neqbit19 : ∀t2.t12 ≠ t2 → eq_bit t12 t2 = false.
1454  #t2; ncases t2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1455 nqed.
1456
1457 nlemma neq_to_neqbit20 : ∀t2.t13 ≠ t2 → eq_bit t13 t2 = false.
1458  #t2; ncases t2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1459 nqed.
1460
1461 nlemma neq_to_neqbit21 : ∀t2.t14 ≠ t2 → eq_bit t14 t2 = false.
1462  #t2; ncases t2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1463 nqed.
1464
1465 nlemma neq_to_neqbit22 : ∀t2.t15 ≠ t2 → eq_bit t15 t2 = false.
1466  #t2; ncases t2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1467 nqed.
1468
1469 nlemma neq_to_neqbit23 : ∀t2.t16 ≠ t2 → eq_bit t16 t2 = false.
1470  #t2; ncases t2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1471 nqed.
1472
1473 nlemma neq_to_neqbit24 : ∀t2.t17 ≠ t2 → eq_bit t17 t2 = false.
1474  #t2; ncases t2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1475 nqed.
1476
1477 nlemma neq_to_neqbit25 : ∀t2.t18 ≠ t2 → eq_bit t18 t2 = false.
1478  #t2; ncases t2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1479 nqed.
1480
1481 nlemma neq_to_neqbit26 : ∀t2.t19 ≠ t2 → eq_bit t19 t2 = false.
1482  #t2; ncases t2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1483 nqed.
1484
1485 nlemma neq_to_neqbit27 : ∀t2.t1A ≠ t2 → eq_bit t1A t2 = false.
1486  #t2; ncases t2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1487 nqed.
1488
1489 nlemma neq_to_neqbit28 : ∀t2.t1B ≠ t2 → eq_bit t1B t2 = false.
1490  #t2; ncases t2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1491 nqed.
1492
1493 nlemma neq_to_neqbit29 : ∀t2.t1C ≠ t2 → eq_bit t1C t2 = false.
1494  #t2; ncases t2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1495 nqed.
1496
1497 nlemma neq_to_neqbit30 : ∀t2.t1D ≠ t2 → eq_bit t1D t2 = false.
1498  #t2; ncases t2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1499 nqed.
1500
1501 nlemma neq_to_neqbit31 : ∀t2.t1E ≠ t2 → eq_bit t1E t2 = false.
1502  #t2; ncases t2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1503 nqed.
1504
1505 nlemma neq_to_neqbit32 : ∀t2.t1F ≠ t2 → eq_bit t1F t2 = false.
1506  #t2; ncases t2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
1507 nqed.
1508
1509 nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
1510  #t1; nelim t1;
1511  ##[ ##1: napply neq_to_neqbit1
1512  ##| ##2: napply neq_to_neqbit2
1513  ##| ##3: napply neq_to_neqbit3
1514  ##| ##4: napply neq_to_neqbit4
1515  ##| ##5: napply neq_to_neqbit5
1516  ##| ##6: napply neq_to_neqbit6
1517  ##| ##7: napply neq_to_neqbit7
1518  ##| ##8: napply neq_to_neqbit8
1519  ##| ##9: napply neq_to_neqbit9
1520  ##| ##10: napply neq_to_neqbit10
1521  ##| ##11: napply neq_to_neqbit11
1522  ##| ##12: napply neq_to_neqbit12
1523  ##| ##13: napply neq_to_neqbit13
1524  ##| ##14: napply neq_to_neqbit14
1525  ##| ##15: napply neq_to_neqbit15
1526  ##| ##16: napply neq_to_neqbit16
1527  ##| ##17: napply neq_to_neqbit17
1528  ##| ##18: napply neq_to_neqbit18
1529  ##| ##19: napply neq_to_neqbit19
1530  ##| ##20: napply neq_to_neqbit20
1531  ##| ##21: napply neq_to_neqbit21
1532  ##| ##22: napply neq_to_neqbit22
1533  ##| ##23: napply neq_to_neqbit23
1534  ##| ##24: napply neq_to_neqbit24
1535  ##| ##25: napply neq_to_neqbit25
1536  ##| ##26: napply neq_to_neqbit26
1537  ##| ##27: napply neq_to_neqbit27
1538  ##| ##28: napply neq_to_neqbit28
1539  ##| ##29: napply neq_to_neqbit29
1540  ##| ##30: napply neq_to_neqbit30
1541  ##| ##31: napply neq_to_neqbit31
1542  ##| ##32: napply neq_to_neqbit32
1543  ##]
1544 nqed.