helm/software/matita/contribs/ng_assembly/freescale/aux_bases_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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/bool_lemmas.ma".
  24 include "freescale/aux_bases.ma".
  25
  26 (* ****** *)
  27 (* OTTALI *)
  28 (* ****** *)
  29
  30 ndefinition oct_destruct_aux ≝
  31 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
  32  match n1 with
  33   [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
  34   | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
  35   | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
  36   | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
  37   | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
  38   | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
  39   | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
  40   | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
  41   ].
  42
  43 ndefinition oct_destruct : oct_destruct_aux.
  44  #n1; #n2; #P;
  45  nelim n1;
  46  ##[ ##1: nelim n2; nnormalize; #H;
  47           ##[ ##1: napply (λx:P.x)
  48           ##| ##*: napply (False_ind (λ_.?) ?);
  49                    nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
  50                    nrewrite > H; nnormalize; napply I
  51           ##]
  52  ##| ##2: nelim n2; nnormalize; #H;
  53           ##[ ##2: napply (λx:P.x)
  54           ##| ##*: napply (False_ind (λ_.?) ?);
  55                    nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
  56                    nrewrite > H; nnormalize; napply I
  57           ##]
  58  ##| ##3: nelim n2; nnormalize; #H;
  59           ##[ ##3: napply (λx:P.x)
  60           ##| ##*: napply (False_ind (λ_.?) ?);
  61                    nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
  62                    nrewrite > H; nnormalize; napply I
  63           ##]
  64  ##| ##4: nelim n2; nnormalize; #H;
  65           ##[ ##4: napply (λx:P.x)
  66           ##| ##*: napply (False_ind (λ_.?) ?);
  67                    nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
  68                    nrewrite > H; nnormalize; napply I
  69           ##]
  70  ##| ##5: nelim n2; nnormalize; #H;
  71           ##[ ##5: napply (λx:P.x)
  72           ##| ##*: napply (False_ind (λ_.?) ?);
  73                    nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
  74                    nrewrite > H; nnormalize; napply I
  75           ##]
  76  ##| ##6: nelim n2; nnormalize; #H;
  77           ##[ ##6: napply (λx:P.x)
  78           ##| ##*: napply (False_ind (λ_.?) ?);
  79                    nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
  80                    nrewrite > H; nnormalize; napply I
  81           ##]
  82  ##| ##7: nelim n2; nnormalize; #H;
  83           ##[ ##7: napply (λx:P.x)
  84           ##| ##*: napply (False_ind (λ_.?) ?);
  85                    nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
  86                    nrewrite > H; nnormalize; napply I
  87           ##]
  88  ##| ##8: nelim n2; nnormalize; #H;
  89           ##[ ##8: napply (λx:P.x)
  90           ##| ##*: napply (False_ind (λ_.?) ?);
  91                    nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
  92                    nrewrite > H; nnormalize; napply I
  93           ##]
  94  ##]
  95 nqed.
  96
  97 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
  98  #n1; #n2;
  99  nelim n1;
 100  nelim n2;
 101  nnormalize;
 102  napply (refl_eq ??).
 103 nqed.
 104
 105 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
 106  #n1; #n2;
 107  ncases n1;
 108  ncases n2;
 109  nnormalize;
 110  ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
 111  ##| ##*: #H; napply (bool_destruct ??? H)
 112  ##]
 113 nqed.
 114
 115 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
 116  #n1; #n2;
 117  ncases n1;
 118  ncases n2;
 119  nnormalize;
 120  ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
 121  ##| ##*: #H; napply (oct_destruct ??? H)
 122  ##]
 123 nqed.
 124
 125 (* ************* *)
 126 (* BITRIGESIMALI *)
 127 (* ************* *)
 128
 129 ndefinition bitrigesim_destruct1 :
 130 Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
 131  #t2; #P;
 132  ncases t2;
 133  nnormalize; #H;
 134  ##[ ##1: napply (λx:P.x)
 135  ##| ##*: napply (False_ind (λ_.?) ?);
 136           nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
 137           nrewrite > H; nnormalize; napply I
 138  ##]
 139 nqed.
 140
 141 ndefinition bitrigesim_destruct2 :
 142 Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
 143  #t2; #P;
 144  ncases t2;
 145  nnormalize; #H;
 146  ##[ ##2: napply (λx:P.x)
 147  ##| ##*: napply (False_ind (λ_.?) ?);
 148           nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
 149           nrewrite > H; nnormalize; napply I
 150  ##]
 151 nqed.
 152
 153 ndefinition bitrigesim_destruct3 :
 154 Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
 155  #t2; #P;
 156  ncases t2;
 157  nnormalize; #H;
 158  ##[ ##3: napply (λx:P.x)
 159  ##| ##*: napply (False_ind (λ_.?) ?);
 160           nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
 161           nrewrite > H; nnormalize; napply I
 162  ##]
 163 nqed.
 164
 165 ndefinition bitrigesim_destruct4 :
 166 Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
 167  #t2; #P;
 168  ncases t2;
 169  nnormalize; #H;
 170  ##[ ##4: napply (λx:P.x)
 171  ##| ##*: napply (False_ind (λ_.?) ?);
 172           nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
 173           nrewrite > H; nnormalize; napply I
 174  ##]
 175 nqed.
 176
 177 ndefinition bitrigesim_destruct5 :
 178 Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
 179  #t2; #P;
 180  ncases t2;
 181  nnormalize; #H;
 182  ##[ ##5: napply (λx:P.x)
 183  ##| ##*: napply (False_ind (λ_.?) ?);
 184           nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
 185           nrewrite > H; nnormalize; napply I
 186  ##]
 187 nqed.
 188
 189 ndefinition bitrigesim_destruct6 :
 190 Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
 191  #t2; #P;
 192  ncases t2;
 193  nnormalize; #H;
 194  ##[ ##6: napply (λx:P.x)
 195  ##| ##*: napply (False_ind (λ_.?) ?);
 196           nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
 197           nrewrite > H; nnormalize; napply I
 198  ##]
 199 nqed.
 200
 201 ndefinition bitrigesim_destruct7 :
 202 Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
 203  #t2; #P;
 204  ncases t2;
 205  nnormalize; #H;
 206  ##[ ##7: napply (λx:P.x)
 207  ##| ##*: napply (False_ind (λ_.?) ?);
 208           nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
 209           nrewrite > H; nnormalize; napply I
 210  ##]
 211 nqed.
 212
 213 ndefinition bitrigesim_destruct8 :
 214 Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
 215  #t2; #P;
 216  ncases t2;
 217  nnormalize; #H;
 218  ##[ ##8: napply (λx:P.x)
 219  ##| ##*: napply (False_ind (λ_.?) ?);
 220           nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
 221           nrewrite > H; nnormalize; napply I
 222  ##]
 223 nqed.
 224
 225 ndefinition bitrigesim_destruct9 :
 226 Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
 227  #t2; #P;
 228  ncases t2;
 229  nnormalize; #H;
 230  ##[ ##9: napply (λx:P.x)
 231  ##| ##*: napply (False_ind (λ_.?) ?);
 232           nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
 233           nrewrite > H; nnormalize; napply I
 234  ##]
 235 nqed.
 236
 237 ndefinition bitrigesim_destruct10 :
 238 Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
 239  #t2; #P;
 240  ncases t2;
 241  nnormalize; #H;
 242  ##[ ##10: napply (λx:P.x)
 243  ##| ##*: napply (False_ind (λ_.?) ?);
 244           nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
 245           nrewrite > H; nnormalize; napply I
 246  ##]
 247 nqed.
 248
 249 ndefinition bitrigesim_destruct11 :
 250 Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
 251  #t2; #P;
 252  ncases t2;
 253  nnormalize; #H;
 254  ##[ ##11: napply (λx:P.x)
 255  ##| ##*: napply (False_ind (λ_.?) ?);
 256           nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
 257           nrewrite > H; nnormalize; napply I
 258  ##]
 259 nqed.
 260
 261 ndefinition bitrigesim_destruct12 :
 262 Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
 263  #t2; #P;
 264  ncases t2;
 265  nnormalize; #H;
 266  ##[ ##12: napply (λx:P.x)
 267  ##| ##*: napply (False_ind (λ_.?) ?);
 268           nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
 269           nrewrite > H; nnormalize; napply I
 270  ##]
 271 nqed.
 272
 273 ndefinition bitrigesim_destruct13 :
 274 Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
 275  #t2; #P;
 276  ncases t2;
 277  nnormalize; #H;
 278  ##[ ##13: napply (λx:P.x)
 279  ##| ##*: napply (False_ind (λ_.?) ?);
 280           nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
 281           nrewrite > H; nnormalize; napply I
 282  ##]
 283 nqed.
 284
 285 ndefinition bitrigesim_destruct14 :
 286 Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
 287  #t2; #P;
 288  ncases t2;
 289  nnormalize; #H;
 290  ##[ ##14: napply (λx:P.x)
 291  ##| ##*: napply (False_ind (λ_.?) ?);
 292           nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
 293           nrewrite > H; nnormalize; napply I
 294  ##]
 295 nqed.
 296
 297 ndefinition bitrigesim_destruct15 :
 298 Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
 299  #t2; #P;
 300  ncases t2;
 301  nnormalize; #H;
 302  ##[ ##15: napply (λx:P.x)
 303  ##| ##*: napply (False_ind (λ_.?) ?);
 304           nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
 305           nrewrite > H; nnormalize; napply I
 306  ##]
 307 nqed.
 308
 309 ndefinition bitrigesim_destruct16 :
 310 Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
 311  #t2; #P;
 312  ncases t2;
 313  nnormalize; #H;
 314  ##[ ##16: napply (λx:P.x)
 315  ##| ##*: napply (False_ind (λ_.?) ?);
 316           nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
 317           nrewrite > H; nnormalize; napply I
 318  ##]
 319 nqed.
 320
 321 ndefinition bitrigesim_destruct17 :
 322 Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
 323  #t2; #P;
 324  ncases t2;
 325  nnormalize; #H;
 326  ##[ ##17: napply (λx:P.x)
 327  ##| ##*: napply (False_ind (λ_.?) ?);
 328           nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
 329           nrewrite > H; nnormalize; napply I
 330  ##]
 331 nqed.
 332
 333 ndefinition bitrigesim_destruct18 :
 334 Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
 335  #t2; #P;
 336  ncases t2;
 337  nnormalize; #H;
 338  ##[ ##18: napply (λx:P.x)
 339  ##| ##*: napply (False_ind (λ_.?) ?);
 340           nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
 341           nrewrite > H; nnormalize; napply I
 342  ##]
 343 nqed.
 344
 345 ndefinition bitrigesim_destruct19 :
 346 Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
 347  #t2; #P;
 348  ncases t2;
 349  nnormalize; #H;
 350  ##[ ##19: napply (λx:P.x)
 351  ##| ##*: napply (False_ind (λ_.?) ?);
 352           nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
 353           nrewrite > H; nnormalize; napply I
 354  ##]
 355 nqed.
 356
 357 ndefinition bitrigesim_destruct20 :
 358 Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
 359  #t2; #P;
 360  ncases t2;
 361  nnormalize; #H;
 362  ##[ ##20: napply (λx:P.x)
 363  ##| ##*: napply (False_ind (λ_.?) ?);
 364           nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
 365           nrewrite > H; nnormalize; napply I
 366  ##]
 367 nqed.
 368
 369 ndefinition bitrigesim_destruct21 :
 370 Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
 371  #t2; #P;
 372  ncases t2;
 373  nnormalize; #H;
 374  ##[ ##21: napply (λx:P.x)
 375  ##| ##*: napply (False_ind (λ_.?) ?);
 376           nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
 377           nrewrite > H; nnormalize; napply I
 378  ##]
 379 nqed.
 380
 381 ndefinition bitrigesim_destruct22 :
 382 Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
 383  #t2; #P;
 384  ncases t2;
 385  nnormalize; #H;
 386  ##[ ##22: napply (λx:P.x)
 387  ##| ##*: napply (False_ind (λ_.?) ?);
 388           nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
 389           nrewrite > H; nnormalize; napply I
 390  ##]
 391 nqed.
 392
 393 ndefinition bitrigesim_destruct23 :
 394 Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
 395  #t2; #P;
 396  ncases t2;
 397  nnormalize; #H;
 398  ##[ ##23: napply (λx:P.x)
 399  ##| ##*: napply (False_ind (λ_.?) ?);
 400           nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
 401           nrewrite > H; nnormalize; napply I
 402  ##]
 403 nqed.
 404
 405 ndefinition bitrigesim_destruct24 :
 406 Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
 407  #t2; #P;
 408  ncases t2;
 409  nnormalize; #H;
 410  ##[ ##24: napply (λx:P.x)
 411  ##| ##*: napply (False_ind (λ_.?) ?);
 412           nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
 413           nrewrite > H; nnormalize; napply I
 414  ##]
 415 nqed.
 416
 417 ndefinition bitrigesim_destruct25 :
 418 Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
 419  #t2; #P;
 420  ncases t2;
 421  nnormalize; #H;
 422  ##[ ##25: napply (λx:P.x)
 423  ##| ##*: napply (False_ind (λ_.?) ?);
 424           nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
 425           nrewrite > H; nnormalize; napply I
 426  ##]
 427 nqed.
 428
 429 ndefinition bitrigesim_destruct26 :
 430 Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
 431  #t2; #P;
 432  ncases t2;
 433  nnormalize; #H;
 434  ##[ ##26: napply (λx:P.x)
 435  ##| ##*: napply (False_ind (λ_.?) ?);
 436           nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
 437           nrewrite > H; nnormalize; napply I
 438  ##]
 439 nqed.
 440
 441 ndefinition bitrigesim_destruct27 :
 442 Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
 443  #t2; #P;
 444  ncases t2;
 445  nnormalize; #H;
 446  ##[ ##27: napply (λx:P.x)
 447  ##| ##*: napply (False_ind (λ_.?) ?);
 448           nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
 449           nrewrite > H; nnormalize; napply I
 450  ##]
 451 nqed.
 452
 453 ndefinition bitrigesim_destruct28 :
 454 Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
 455  #t2; #P;
 456  ncases t2;
 457  nnormalize; #H;
 458  ##[ ##28: napply (λx:P.x)
 459  ##| ##*: napply (False_ind (λ_.?) ?);
 460           nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
 461           nrewrite > H; nnormalize; napply I
 462  ##]
 463 nqed.
 464
 465 ndefinition bitrigesim_destruct29 :
 466 Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
 467  #t2; #P;
 468  ncases t2;
 469  nnormalize; #H;
 470  ##[ ##29: napply (λx:P.x)
 471  ##| ##*: napply (False_ind (λ_.?) ?);
 472           nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
 473           nrewrite > H; nnormalize; napply I
 474  ##]
 475 nqed.
 476
 477 ndefinition bitrigesim_destruct30 :
 478 Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
 479  #t2; #P;
 480  ncases t2;
 481  nnormalize; #H;
 482  ##[ ##30: napply (λx:P.x)
 483  ##| ##*: napply (False_ind (λ_.?) ?);
 484           nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
 485           nrewrite > H; nnormalize; napply I
 486  ##]
 487 nqed.
 488
 489 ndefinition bitrigesim_destruct31 :
 490 Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
 491  #t2; #P;
 492  ncases t2;
 493  nnormalize; #H;
 494  ##[ ##31: napply (λx:P.x)
 495  ##| ##*: napply (False_ind (λ_.?) ?);
 496           nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
 497           nrewrite > H; nnormalize; napply I
 498  ##]
 499 nqed.
 500
 501 ndefinition bitrigesim_destruct32 :
 502 Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
 503  #t2; #P;
 504  ncases t2;
 505  nnormalize; #H;
 506  ##[ ##32: napply (λx:P.x)
 507  ##| ##*: napply (False_ind (λ_.?) ?);
 508           nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
 509           nrewrite > H; nnormalize; napply I
 510  ##]
 511 nqed.
 512
 513 ndefinition bitrigesim_destruct_aux ≝
 514 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
 515  match t1 with
 516   [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
 517   | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
 518   | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
 519   | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
 520   | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
 521   | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
 522   | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
 523   | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
 524   | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
 525   | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
 526   | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
 527   | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
 528   | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
 529   | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
 530   | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
 531   | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
 532   | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
 533   | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
 534   | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
 535   | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
 536   | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
 537   | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
 538   | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
 539   | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
 540   | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
 541   | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
 542   | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
 543   | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
 544   | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
 545   | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
 546   | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
 547   | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
 548   ].
 549
 550 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
 551  #t1;
 552  ncases t1;
 553  ##[ ##1: napply bitrigesim_destruct1
 554  ##| ##2: napply bitrigesim_destruct2
 555  ##| ##3: napply bitrigesim_destruct3
 556  ##| ##4: napply bitrigesim_destruct4
 557  ##| ##5: napply bitrigesim_destruct5
 558  ##| ##6: napply bitrigesim_destruct6
 559  ##| ##7: napply bitrigesim_destruct7
 560  ##| ##8: napply bitrigesim_destruct8
 561  ##| ##9: napply bitrigesim_destruct9
 562  ##| ##10: napply bitrigesim_destruct10
 563  ##| ##11: napply bitrigesim_destruct11
 564  ##| ##12: napply bitrigesim_destruct12
 565  ##| ##13: napply bitrigesim_destruct13
 566  ##| ##14: napply bitrigesim_destruct14
 567  ##| ##15: napply bitrigesim_destruct15
 568  ##| ##16: napply bitrigesim_destruct16
 569  ##| ##17: napply bitrigesim_destruct17
 570  ##| ##18: napply bitrigesim_destruct18
 571  ##| ##19: napply bitrigesim_destruct19
 572  ##| ##20: napply bitrigesim_destruct20
 573  ##| ##21: napply bitrigesim_destruct21
 574  ##| ##22: napply bitrigesim_destruct22
 575  ##| ##23: napply bitrigesim_destruct23
 576  ##| ##24: napply bitrigesim_destruct24
 577  ##| ##25: napply bitrigesim_destruct25
 578  ##| ##26: napply bitrigesim_destruct26
 579  ##| ##27: napply bitrigesim_destruct27
 580  ##| ##28: napply bitrigesim_destruct28
 581  ##| ##29: napply bitrigesim_destruct29
 582  ##| ##30: napply bitrigesim_destruct30
 583  ##| ##31: napply bitrigesim_destruct31
 584  ##| ##32: napply bitrigesim_destruct32
 585  ##]
 586 nqed.
 587
 588 nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
 589  #t1;
 590  nelim t1;
 591  ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 592  ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 593  ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 594  ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 595  ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 596  ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 597  ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 598  ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 599  ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 600  ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 601  ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 602  ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 603  ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 604  ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 605  ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 606  ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 607  ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 608  ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 609  ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 610  ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 611  ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 612  ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 613  ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 614  ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 615  ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 616  ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 617  ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 618  ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 619  ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 620  ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 621  ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 622  ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 623  ##]
 624 nqed.
 625
 626 nlemma eqbitrig_to_eq1 : ∀t2.eq_bitrig t00 t2 = true → t00 = t2.
 627  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 628 nqed.
 629
 630 nlemma eqbitrig_to_eq2 : ∀t2.eq_bitrig t01 t2 = true → t01 = t2.
 631  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 632 nqed.
 633
 634 nlemma eqbitrig_to_eq3 : ∀t2.eq_bitrig t02 t2 = true → t02 = t2.
 635  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 636 nqed.
 637
 638 nlemma eqbitrig_to_eq4 : ∀t2.eq_bitrig t03 t2 = true → t03 = t2.
 639  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 640 nqed.
 641
 642 nlemma eqbitrig_to_eq5 : ∀t2.eq_bitrig t04 t2 = true → t04 = t2.
 643  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 644 nqed.
 645
 646 nlemma eqbitrig_to_eq6 : ∀t2.eq_bitrig t05 t2 = true → t05 = t2.
 647  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 648 nqed.
 649
 650 nlemma eqbitrig_to_eq7 : ∀t2.eq_bitrig t06 t2 = true → t06 = t2.
 651  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 652 nqed.
 653
 654 nlemma eqbitrig_to_eq8 : ∀t2.eq_bitrig t07 t2 = true → t07 = t2.
 655  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 656 nqed.
 657
 658 nlemma eqbitrig_to_eq9 : ∀t2.eq_bitrig t08 t2 = true → t08 = t2.
 659  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 660 nqed.
 661
 662 nlemma eqbitrig_to_eq10 : ∀t2.eq_bitrig t09 t2 = true → t09 = t2.
 663  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 664 nqed.
 665
 666 nlemma eqbitrig_to_eq11 : ∀t2.eq_bitrig t0A t2 = true → t0A = t2.
 667  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 668 nqed.
 669
 670 nlemma eqbitrig_to_eq12 : ∀t2.eq_bitrig t0B t2 = true → t0B = t2.
 671  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 672 nqed.
 673
 674 nlemma eqbitrig_to_eq13 : ∀t2.eq_bitrig t0C t2 = true → t0C = t2.
 675  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 676 nqed.
 677
 678 nlemma eqbitrig_to_eq14 : ∀t2.eq_bitrig t0D t2 = true → t0D = t2.
 679  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 680 nqed.
 681
 682 nlemma eqbitrig_to_eq15 : ∀t2.eq_bitrig t0E t2 = true → t0E = t2.
 683  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 684 nqed.
 685
 686 nlemma eqbitrig_to_eq16 : ∀t2.eq_bitrig t0F t2 = true → t0F = t2.
 687  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 688 nqed.
 689
 690 nlemma eqbitrig_to_eq17 : ∀t2.eq_bitrig t10 t2 = true → t10 = t2.
 691  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 692 nqed.
 693
 694 nlemma eqbitrig_to_eq18 : ∀t2.eq_bitrig t11 t2 = true → t11 = t2.
 695  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 696 nqed.
 697
 698 nlemma eqbitrig_to_eq19 : ∀t2.eq_bitrig t12 t2 = true → t12 = t2.
 699  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 700 nqed.
 701
 702 nlemma eqbitrig_to_eq20 : ∀t2.eq_bitrig t13 t2 = true → t13 = t2.
 703  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 704 nqed.
 705
 706 nlemma eqbitrig_to_eq21 : ∀t2.eq_bitrig t14 t2 = true → t14 = t2.
 707  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 708 nqed.
 709
 710 nlemma eqbitrig_to_eq22 : ∀t2.eq_bitrig t15 t2 = true → t15 = t2.
 711  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 712 nqed.
 713
 714 nlemma eqbitrig_to_eq23 : ∀t2.eq_bitrig t16 t2 = true → t16 = t2.
 715  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 716 nqed.
 717
 718 nlemma eqbitrig_to_eq24 : ∀t2.eq_bitrig t17 t2 = true → t17 = t2.
 719  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 720 nqed.
 721
 722 nlemma eqbitrig_to_eq25 : ∀t2.eq_bitrig t18 t2 = true → t18 = t2.
 723  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 724 nqed.
 725
 726 nlemma eqbitrig_to_eq26 : ∀t2.eq_bitrig t19 t2 = true → t19 = t2.
 727  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 728 nqed.
 729
 730 nlemma eqbitrig_to_eq27 : ∀t2.eq_bitrig t1A t2 = true → t1A = t2.
 731  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 732 nqed.
 733
 734 nlemma eqbitrig_to_eq28 : ∀t2.eq_bitrig t1B t2 = true → t1B = t2.
 735  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 736 nqed.
 737
 738 nlemma eqbitrig_to_eq29 : ∀t2.eq_bitrig t1C t2 = true → t1C = t2.
 739  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 740 nqed.
 741
 742 nlemma eqbitrig_to_eq30 : ∀t2.eq_bitrig t1D t2 = true → t1D = t2.
 743  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 744 nqed.
 745
 746 nlemma eqbitrig_to_eq31 : ∀t2.eq_bitrig t1E t2 = true → t1E = t2.
 747  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 748 nqed.
 749
 750 nlemma eqbitrig_to_eq32 : ∀t2.eq_bitrig t1F t2 = true → t1F = t2.
 751  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
 752 nqed.
 753
 754 nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
 755  #t1;
 756  ncases t1;
 757  ##[ ##1: napply eqbitrig_to_eq1
 758  ##| ##2: napply eqbitrig_to_eq2
 759  ##| ##3: napply eqbitrig_to_eq3
 760  ##| ##4: napply eqbitrig_to_eq4
 761  ##| ##5: napply eqbitrig_to_eq5
 762  ##| ##6: napply eqbitrig_to_eq6
 763  ##| ##7: napply eqbitrig_to_eq7
 764  ##| ##8: napply eqbitrig_to_eq8
 765  ##| ##9: napply eqbitrig_to_eq9
 766  ##| ##10: napply eqbitrig_to_eq10
 767  ##| ##11: napply eqbitrig_to_eq11
 768  ##| ##12: napply eqbitrig_to_eq12
 769  ##| ##13: napply eqbitrig_to_eq13
 770  ##| ##14: napply eqbitrig_to_eq14
 771  ##| ##15: napply eqbitrig_to_eq15
 772  ##| ##16: napply eqbitrig_to_eq16
 773  ##| ##17: napply eqbitrig_to_eq17
 774  ##| ##18: napply eqbitrig_to_eq18
 775  ##| ##19: napply eqbitrig_to_eq19
 776  ##| ##20: napply eqbitrig_to_eq20
 777  ##| ##21: napply eqbitrig_to_eq21
 778  ##| ##22: napply eqbitrig_to_eq22
 779  ##| ##23: napply eqbitrig_to_eq23
 780  ##| ##24: napply eqbitrig_to_eq24
 781  ##| ##25: napply eqbitrig_to_eq25
 782  ##| ##26: napply eqbitrig_to_eq26
 783  ##| ##27: napply eqbitrig_to_eq27
 784  ##| ##28: napply eqbitrig_to_eq28
 785  ##| ##29: napply eqbitrig_to_eq29
 786  ##| ##30: napply eqbitrig_to_eq30
 787  ##| ##31: napply eqbitrig_to_eq31
 788  ##| ##32: napply eqbitrig_to_eq32
 789  ##]
 790 nqed.
 791
 792 nlemma eq_to_eqbitrig1 : ∀t2.t00 = t2 → eq_bitrig t00 t2 = true.
 793  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 794 nqed.
 795
 796 nlemma eq_to_eqbitrig2 : ∀t2.t01 = t2 → eq_bitrig t01 t2 = true.
 797  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 798 nqed.
 799
 800 nlemma eq_to_eqbitrig3 : ∀t2.t02 = t2 → eq_bitrig t02 t2 = true.
 801  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 802 nqed.
 803
 804 nlemma eq_to_eqbitrig4 : ∀t2.t03 = t2 → eq_bitrig t03 t2 = true.
 805  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 806 nqed.
 807
 808 nlemma eq_to_eqbitrig5 : ∀t2.t04 = t2 → eq_bitrig t04 t2 = true.
 809  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 810 nqed.
 811
 812 nlemma eq_to_eqbitrig6 : ∀t2.t05 = t2 → eq_bitrig t05 t2 = true.
 813  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 814 nqed.
 815
 816 nlemma eq_to_eqbitrig7 : ∀t2.t06 = t2 → eq_bitrig t06 t2 = true.
 817  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 818 nqed.
 819
 820 nlemma eq_to_eqbitrig8 : ∀t2.t07 = t2 → eq_bitrig t07 t2 = true.
 821  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 822 nqed.
 823
 824 nlemma eq_to_eqbitrig9 : ∀t2.t08 = t2 → eq_bitrig t08 t2 = true.
 825  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 826 nqed.
 827
 828 nlemma eq_to_eqbitrig10 : ∀t2.t09 = t2 → eq_bitrig t09 t2 = true.
 829  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 830 nqed.
 831
 832 nlemma eq_to_eqbitrig11 : ∀t2.t0A = t2 → eq_bitrig t0A t2 = true.
 833  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 834 nqed.
 835
 836 nlemma eq_to_eqbitrig12 : ∀t2.t0B = t2 → eq_bitrig t0B t2 = true.
 837  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 838 nqed.
 839
 840 nlemma eq_to_eqbitrig13 : ∀t2.t0C = t2 → eq_bitrig t0C t2 = true.
 841  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 842 nqed.
 843
 844 nlemma eq_to_eqbitrig14 : ∀t2.t0D = t2 → eq_bitrig t0D t2 = true.
 845  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 846 nqed.
 847
 848 nlemma eq_to_eqbitrig15 : ∀t2.t0E = t2 → eq_bitrig t0E t2 = true.
 849  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 850 nqed.
 851
 852 nlemma eq_to_eqbitrig16 : ∀t2.t0F = t2 → eq_bitrig t0F t2 = true.
 853  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 854 nqed.
 855
 856 nlemma eq_to_eqbitrig17 : ∀t2.t10 = t2 → eq_bitrig t10 t2 = true.
 857  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 858 nqed.
 859
 860 nlemma eq_to_eqbitrig18 : ∀t2.t11 = t2 → eq_bitrig t11 t2 = true.
 861  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 862 nqed.
 863
 864 nlemma eq_to_eqbitrig19 : ∀t2.t12 = t2 → eq_bitrig t12 t2 = true.
 865  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 866 nqed.
 867
 868 nlemma eq_to_eqbitrig20 : ∀t2.t13 = t2 → eq_bitrig t13 t2 = true.
 869  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 870 nqed.
 871
 872 nlemma eq_to_eqbitrig21 : ∀t2.t14 = t2 → eq_bitrig t14 t2 = true.
 873  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 874 nqed.
 875 nlemma eq_to_eqbitrig22 : ∀t2.t15 = t2 → eq_bitrig t15 t2 = true.
 876  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 877 nqed.
 878
 879 nlemma eq_to_eqbitrig23 : ∀t2.t16 = t2 → eq_bitrig t16 t2 = true.
 880  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 881 nqed.
 882
 883 nlemma eq_to_eqbitrig24 : ∀t2.t17 = t2 → eq_bitrig t17 t2 = true.
 884  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 885 nqed.
 886
 887 nlemma eq_to_eqbitrig25 : ∀t2.t18 = t2 → eq_bitrig t18 t2 = true.
 888  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 889 nqed.
 890
 891 nlemma eq_to_eqbitrig26 : ∀t2.t19 = t2 → eq_bitrig t19 t2 = true.
 892  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 893 nqed.
 894
 895 nlemma eq_to_eqbitrig27 : ∀t2.t1A = t2 → eq_bitrig t1A t2 = true.
 896  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 897 nqed.
 898
 899 nlemma eq_to_eqbitrig28 : ∀t2.t1B = t2 → eq_bitrig t1B t2 = true.
 900  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 901 nqed.
 902
 903 nlemma eq_to_eqbitrig29 : ∀t2.t1C = t2 → eq_bitrig t1C t2 = true.
 904  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 905 nqed.
 906
 907 nlemma eq_to_eqbitrig30 : ∀t2.t1D = t2 → eq_bitrig t1D t2 = true.
 908  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 909 nqed.
 910
 911 nlemma eq_to_eqbitrig31 : ∀t2.t1E = t2 → eq_bitrig t1E t2 = true.
 912  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 913 nqed.
 914
 915 nlemma eq_to_eqbitrig32 : ∀t2.t1F = t2 → eq_bitrig t1F t2 = true.
 916  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
 917 nqed.
 918
 919 nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
 920  #t1;
 921  ncases t1;
 922  ##[ ##1: napply eq_to_eqbitrig1
 923  ##| ##2: napply eq_to_eqbitrig2
 924  ##| ##3: napply eq_to_eqbitrig3
 925  ##| ##4: napply eq_to_eqbitrig4
 926  ##| ##5: napply eq_to_eqbitrig5
 927  ##| ##6: napply eq_to_eqbitrig6
 928  ##| ##7: napply eq_to_eqbitrig7
 929  ##| ##8: napply eq_to_eqbitrig8
 930  ##| ##9: napply eq_to_eqbitrig9
 931  ##| ##10: napply eq_to_eqbitrig10
 932  ##| ##11: napply eq_to_eqbitrig11
 933  ##| ##12: napply eq_to_eqbitrig12
 934  ##| ##13: napply eq_to_eqbitrig13
 935  ##| ##14: napply eq_to_eqbitrig14
 936  ##| ##15: napply eq_to_eqbitrig15
 937  ##| ##16: napply eq_to_eqbitrig16
 938  ##| ##17: napply eq_to_eqbitrig17
 939  ##| ##18: napply eq_to_eqbitrig18
 940  ##| ##19: napply eq_to_eqbitrig19
 941  ##| ##20: napply eq_to_eqbitrig20
 942  ##| ##21: napply eq_to_eqbitrig21
 943  ##| ##22: napply eq_to_eqbitrig22
 944  ##| ##23: napply eq_to_eqbitrig23
 945  ##| ##24: napply eq_to_eqbitrig24
 946  ##| ##25: napply eq_to_eqbitrig25
 947  ##| ##26: napply eq_to_eqbitrig26
 948  ##| ##27: napply eq_to_eqbitrig27
 949  ##| ##28: napply eq_to_eqbitrig28
 950  ##| ##29: napply eq_to_eqbitrig29
 951  ##| ##30: napply eq_to_eqbitrig30
 952  ##| ##31: napply eq_to_eqbitrig31
 953  ##| ##32: napply eq_to_eqbitrig32
 954  ##]
 955 nqed.