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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/bool_lemmas.ma".
  28 include "freescale/aux_bases.ma".
  29
  30 (* ****** *)
  31 (* OTTALI *)
  32 (* ****** *)
  33
  34 ndefinition oct_destruct :
  35  Πn1,n2:oct.ΠP:Prop.n1 = n2 →
  36  match n1 with
  37   [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
  38   | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
  39   | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
  40   | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
  41   | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
  42   | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
  43   | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
  44   | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
  45   ].
  46  #n1; #n2; #P;
  47  nelim n1;
  48  ##[ ##1: nelim n2; nnormalize; #H;
  49           ##[ ##1: napply (λx:P.x)
  50           ##| ##*: napply (False_ind ??);
  51                    nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
  52                    nrewrite > H; nnormalize; napply I
  53           ##]
  54  ##| ##2: nelim n2; nnormalize; #H;
  55           ##[ ##2: napply (λx:P.x)
  56           ##| ##*: napply (False_ind ??);
  57                    nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
  58                    nrewrite > H; nnormalize; napply I
  59           ##]
  60  ##| ##3: nelim n2; nnormalize; #H;
  61           ##[ ##3: napply (λx:P.x)
  62           ##| ##*: napply (False_ind ??);
  63                    nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
  64                    nrewrite > H; nnormalize; napply I
  65           ##]
  66  ##| ##4: nelim n2; nnormalize; #H;
  67           ##[ ##4: napply (λx:P.x)
  68           ##| ##*: napply (False_ind ??);
  69                    nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
  70                    nrewrite > H; nnormalize; napply I
  71           ##]
  72  ##| ##5: nelim n2; nnormalize; #H;
  73           ##[ ##5: napply (λx:P.x)
  74           ##| ##*: napply (False_ind ??);
  75                    nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
  76                    nrewrite > H; nnormalize; napply I
  77           ##]
  78  ##| ##6: nelim n2; nnormalize; #H;
  79           ##[ ##6: napply (λx:P.x)
  80           ##| ##*: napply (False_ind ??);
  81                    nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
  82                    nrewrite > H; nnormalize; napply I
  83           ##]
  84  ##| ##7: nelim n2; nnormalize; #H;
  85           ##[ ##7: napply (λx:P.x)
  86           ##| ##*: napply (False_ind ??);
  87                    nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
  88                    nrewrite > H; nnormalize; napply I
  89           ##]
  90  ##| ##8: nelim n2; nnormalize; #H;
  91           ##[ ##8: napply (λx:P.x)
  92           ##| ##*: napply (False_ind ??);
  93                    nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
  94                    nrewrite > H; nnormalize; napply I
  95           ##]
  96  ##]
  97 nqed.
  98
  99 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
 100  #n1; #n2;
 101  nelim n1;
 102  nelim n2;
 103  nnormalize;
 104  napply (refl_eq ??).
 105 nqed.
 106
 107 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
 108  #n1; #n2;
 109  ncases n1;
 110  ncases n2;
 111  nnormalize;
 112  ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
 113  ##| ##*: #H; napply (bool_destruct ??? H)
 114  ##]
 115 nqed.
 116
 117 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
 118  #n1; #n2;
 119  ncases n1;
 120  ncases n2;
 121  nnormalize;
 122  ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
 123  ##| ##*: #H; napply (oct_destruct ??? H)
 124  ##]
 125 nqed.
 126
 127 (* ************* *)
 128 (* BITRIGESIMALI *)
 129 (* ************* *)
 130
 131 ndefinition bitrigesim_destruct :
 132  Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
 133  match t1 with
 134   [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
 135   | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
 136   | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
 137   | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
 138   | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
 139   | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
 140   | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
 141   | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
 142   | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
 143   | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
 144   | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
 145   | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
 146   | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
 147   | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
 148   | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
 149   | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
 150   | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
 151   | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
 152   | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
 153   | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
 154   | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
 155   | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
 156   | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
 157   | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
 158   | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
 159   | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
 160   | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
 161   | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
 162   | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
 163   | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
 164   | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
 165   | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
 166   ].
 167  #t1; #t2; #P;
 168  nelim t1;
 169  ##[ ##1: nelim t2; nnormalize; #H;
 170           ##[ ##1: napply (λx:P.x)
 171           ##| ##*: napply (False_ind ??);
 172                    nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
 173                    nrewrite > H; nnormalize; napply I
 174           ##]
 175  ##| ##2: nelim t2; nnormalize; #H;
 176           ##[ ##2: napply (λx:P.x)
 177           ##| ##*: napply (False_ind ??);
 178                    nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
 179                    nrewrite > H; nnormalize; napply I
 180           ##]
 181  ##| ##3: nelim t2; nnormalize; #H;
 182           ##[ ##3: napply (λx:P.x)
 183           ##| ##*: napply (False_ind ??);
 184                    nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
 185                    nrewrite > H; nnormalize; napply I
 186           ##]
 187  ##| ##4: nelim t2; nnormalize; #H;
 188           ##[ ##4: napply (λx:P.x)
 189           ##| ##*: napply (False_ind ??);
 190                    nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
 191                    nrewrite > H; nnormalize; napply I
 192           ##]
 193  ##| ##5: nelim t2; nnormalize; #H;
 194           ##[ ##5: napply (λx:P.x)
 195           ##| ##*: napply (False_ind ??);
 196                    nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
 197                    nrewrite > H; nnormalize; napply I
 198           ##]
 199  ##| ##6: nelim t2; nnormalize; #H;
 200           ##[ ##6: napply (λx:P.x)
 201           ##| ##*: napply (False_ind ??);
 202                    nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
 203                    nrewrite > H; nnormalize; napply I
 204           ##]
 205  ##| ##7: nelim t2; 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  ##| ##8: nelim t2; nnormalize; #H;
 212           ##[ ##8: napply (λx:P.x)
 213           ##| ##*: napply (False_ind ??);
 214                    nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
 215                    nrewrite > H; nnormalize; napply I
 216           ##]
 217  ##| ##9: nelim t2; nnormalize; #H;
 218           ##[ ##9: napply (λx:P.x)
 219           ##| ##*: napply (False_ind ??);
 220                    nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
 221                    nrewrite > H; nnormalize; napply I
 222           ##]
 223  ##| ##10: nelim t2; nnormalize; #H;
 224           ##[ ##10: napply (λx:P.x)
 225           ##| ##*: napply (False_ind ??);
 226                    nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
 227                    nrewrite > H; nnormalize; napply I
 228           ##]
 229  ##| ##11: nelim t2; nnormalize; #H;
 230           ##[ ##11: napply (λx:P.x)
 231           ##| ##*: napply (False_ind ??);
 232                    nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
 233                    nrewrite > H; nnormalize; napply I
 234           ##]
 235  ##| ##12: nelim t2; nnormalize; #H;
 236           ##[ ##12: napply (λx:P.x)
 237           ##| ##*: napply (False_ind ??);
 238                    nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
 239                    nrewrite > H; nnormalize; napply I
 240           ##]
 241  ##| ##13: nelim t2; nnormalize; #H;
 242           ##[ ##13: napply (λx:P.x)
 243           ##| ##*: napply (False_ind ??);
 244                    nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
 245                    nrewrite > H; nnormalize; napply I
 246           ##]
 247  ##| ##14: nelim t2; nnormalize; #H;
 248           ##[ ##14: napply (λx:P.x)
 249           ##| ##*: napply (False_ind ??);
 250                    nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
 251                    nrewrite > H; nnormalize; napply I
 252           ##]
 253  ##| ##15: nelim t2; nnormalize; #H;
 254           ##[ ##15: napply (λx:P.x)
 255           ##| ##*: napply (False_ind ??);
 256                    nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
 257                    nrewrite > H; nnormalize; napply I
 258           ##]
 259  ##| ##16: nelim t2; nnormalize; #H;
 260           ##[ ##16: napply (λx:P.x)
 261           ##| ##*: napply (False_ind ??);
 262                    nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
 263                    nrewrite > H; nnormalize; napply I
 264           ##]
 265  ##| ##17: nelim t2; nnormalize; #H;
 266           ##[ ##17: napply (λx:P.x)
 267           ##| ##*: napply (False_ind ??);
 268                    nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
 269                    nrewrite > H; nnormalize; napply I
 270           ##]
 271  ##| ##18: nelim t2; nnormalize; #H;
 272           ##[ ##18: napply (λx:P.x)
 273           ##| ##*: napply (False_ind ??);
 274                    nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
 275                    nrewrite > H; nnormalize; napply I
 276           ##]
 277  ##| ##19: nelim t2; nnormalize; #H;
 278           ##[ ##19: napply (λx:P.x)
 279           ##| ##*: napply (False_ind ??);
 280                    nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
 281                    nrewrite > H; nnormalize; napply I
 282           ##]
 283  ##| ##20: nelim t2; nnormalize; #H;
 284           ##[ ##20: napply (λx:P.x)
 285           ##| ##*: napply (False_ind ??);
 286                    nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
 287                    nrewrite > H; nnormalize; napply I
 288           ##]
 289  ##| ##21: nelim t2; nnormalize; #H;
 290           ##[ ##21: napply (λx:P.x)
 291           ##| ##*: napply (False_ind ??);
 292                    nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
 293                    nrewrite > H; nnormalize; napply I
 294           ##]
 295  ##| ##22: nelim t2; nnormalize; #H;
 296           ##[ ##22: napply (λx:P.x)
 297           ##| ##*: napply (False_ind ??);
 298                    nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
 299                    nrewrite > H; nnormalize; napply I
 300           ##]
 301  ##| ##23: nelim t2; nnormalize; #H;
 302           ##[ ##23: napply (λx:P.x)
 303           ##| ##*: napply (False_ind ??);
 304                    nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
 305                    nrewrite > H; nnormalize; napply I
 306           ##]
 307  ##| ##24: nelim t2; nnormalize; #H;
 308           ##[ ##24: napply (λx:P.x)
 309           ##| ##*: napply (False_ind ??);
 310                    nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
 311                    nrewrite > H; nnormalize; napply I
 312           ##]
 313  ##| ##25: nelim t2; nnormalize; #H;
 314           ##[ ##25: napply (λx:P.x)
 315           ##| ##*: napply (False_ind ??);
 316                    nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
 317                    nrewrite > H; nnormalize; napply I
 318           ##]
 319  ##| ##26: nelim t2; nnormalize; #H;
 320           ##[ ##26: napply (λx:P.x)
 321           ##| ##*: napply (False_ind ??);
 322                    nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
 323                    nrewrite > H; nnormalize; napply I
 324           ##]
 325  ##| ##27: nelim t2; nnormalize; #H;
 326           ##[ ##27: napply (λx:P.x)
 327           ##| ##*: napply (False_ind ??);
 328                    nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
 329                    nrewrite > H; nnormalize; napply I
 330           ##]
 331  ##| ##28: nelim t2; nnormalize; #H;
 332           ##[ ##28: napply (λx:P.x)
 333           ##| ##*: napply (False_ind ??);
 334                    nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
 335                    nrewrite > H; nnormalize; napply I
 336           ##]
 337  ##| ##29: nelim t2; nnormalize; #H;
 338           ##[ ##29: napply (λx:P.x)
 339           ##| ##*: napply (False_ind ??);
 340                    nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
 341                    nrewrite > H; nnormalize; napply I
 342           ##]
 343  ##| ##30: nelim t2; nnormalize; #H;
 344           ##[ ##30: napply (λx:P.x)
 345           ##| ##*: napply (False_ind ??);
 346                    nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
 347                    nrewrite > H; nnormalize; napply I
 348           ##]
 349  ##| ##31: nelim t2; nnormalize; #H;
 350           ##[ ##31: napply (λx:P.x)
 351           ##| ##*: napply (False_ind ??);
 352                    nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
 353                    nrewrite > H; nnormalize; napply I
 354           ##]
 355  ##| ##32: nelim t2; nnormalize; #H;
 356           ##[ ##32: napply (λx:P.x)
 357           ##| ##*: napply (False_ind ??);
 358                    nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
 359                    nrewrite > H; nnormalize; napply I
 360           ##]
 361  ##]
 362 nqed.
 363
 364 nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
 365  #t1;
 366  nelim t1;
 367  ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 368  ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 369  ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 370  ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 371  ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 372  ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 373  ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 374  ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 375  ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 376  ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 377  ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 378  ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 379  ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 380  ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 381  ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 382  ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 383  ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 384  ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 385  ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 386  ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 387  ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 388  ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 389  ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 390  ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 391  ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 392  ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 393  ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 394  ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 395  ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 396  ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 397  ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 398  ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
 399  ##]
 400 nqed.
 401
 402 nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
 403  #t1; #t2;
 404  ncases t1;
 405  ##[ ##1: ncases t2; nnormalize; #H;
 406           ##[ ##1: napply (refl_eq ??)
 407           ##| ##*: napply (bool_destruct ??? H)
 408           ##]
 409  ##| ##2: ncases t2; nnormalize; #H;
 410           ##[ ##2: napply (refl_eq ??)
 411           ##| ##*: napply (bool_destruct ??? H)
 412           ##]
 413  ##| ##3: ncases t2; nnormalize; #H;
 414           ##[ ##3: napply (refl_eq ??)
 415           ##| ##*: napply (bool_destruct ??? H)
 416           ##]
 417  ##| ##4: ncases t2; nnormalize; #H;
 418           ##[ ##4: napply (refl_eq ??)
 419           ##| ##*: napply (bool_destruct ??? H)
 420           ##]
 421  ##| ##5: ncases t2; nnormalize; #H;
 422           ##[ ##5: napply (refl_eq ??)
 423           ##| ##*: napply (bool_destruct ??? H)
 424           ##]
 425  ##| ##6: ncases t2; nnormalize; #H;
 426           ##[ ##6: napply (refl_eq ??)
 427           ##| ##*:napply (bool_destruct ??? H)
 428           ##]
 429  ##| ##7: ncases t2; nnormalize; #H;
 430           ##[ ##7: napply (refl_eq ??)
 431           ##| ##*: napply (bool_destruct ??? H)
 432           ##]
 433  ##| ##8: ncases t2; nnormalize; #H;
 434           ##[ ##8: napply (refl_eq ??)
 435           ##| ##*: napply (bool_destruct ??? H)
 436           ##]
 437  ##| ##9: ncases t2; nnormalize; #H;
 438           ##[ ##9: napply (refl_eq ??)
 439           ##| ##*: napply (bool_destruct ??? H)
 440           ##]
 441  ##| ##10: ncases t2; nnormalize; #H;
 442           ##[ ##10: napply (refl_eq ??)
 443           ##| ##*: napply (bool_destruct ??? H)
 444           ##]
 445  ##| ##11: ncases t2; nnormalize; #H;
 446           ##[ ##11: napply (refl_eq ??)
 447           ##| ##*: napply (bool_destruct ??? H)
 448           ##]
 449  ##| ##12: ncases t2; nnormalize; #H;
 450           ##[ ##12: napply (refl_eq ??)
 451           ##| ##*: napply (bool_destruct ??? H)
 452           ##]
 453  ##| ##13: ncases t2; nnormalize; #H;
 454           ##[ ##13: napply (refl_eq ??)
 455           ##| ##*: napply (bool_destruct ??? H)
 456           ##]
 457  ##| ##14: ncases t2; nnormalize; #H;
 458           ##[ ##14: napply (refl_eq ??)
 459           ##| ##*: napply (bool_destruct ??? H)
 460           ##]
 461  ##| ##15: ncases t2; nnormalize; #H;
 462           ##[ ##15: napply (refl_eq ??)
 463           ##| ##*: napply (bool_destruct ??? H)
 464           ##]
 465  ##| ##16: ncases t2; nnormalize; #H;
 466           ##[ ##16: napply (refl_eq ??)
 467           ##| ##*: napply (bool_destruct ??? H)
 468           ##]
 469  ##| ##17: ncases t2; nnormalize; #H;
 470           ##[ ##17: napply (refl_eq ??)
 471           ##| ##*: napply (bool_destruct ??? H)
 472           ##]
 473  ##| ##18: ncases t2; nnormalize; #H;
 474           ##[ ##18: napply (refl_eq ??)
 475           ##| ##*: napply (bool_destruct ??? H)
 476           ##]
 477  ##| ##19: ncases t2; nnormalize; #H;
 478           ##[ ##19: napply (refl_eq ??)
 479           ##| ##*: napply (bool_destruct ??? H)
 480           ##]
 481  ##| ##20: ncases t2; nnormalize; #H;
 482           ##[ ##20: napply (refl_eq ??)
 483           ##| ##*: napply (bool_destruct ??? H)
 484           ##]
 485  ##| ##21: ncases t2; nnormalize; #H;
 486           ##[ ##21: napply (refl_eq ??)
 487           ##| ##*: napply (bool_destruct ??? H)
 488           ##]
 489  ##| ##22: ncases t2; nnormalize; #H;
 490           ##[ ##22: napply (refl_eq ??)
 491           ##| ##*: napply (bool_destruct ??? H)
 492           ##]
 493  ##| ##23: ncases t2; nnormalize; #H;
 494           ##[ ##23: napply (refl_eq ??)
 495           ##| ##*: napply (bool_destruct ??? H)
 496           ##]
 497  ##| ##24: ncases t2; nnormalize; #H;
 498           ##[ ##24: napply (refl_eq ??)
 499           ##| ##*: napply (bool_destruct ??? H)
 500           ##]
 501  ##| ##25: ncases t2; nnormalize; #H;
 502           ##[ ##25: napply (refl_eq ??)
 503           ##| ##*: napply (bool_destruct ??? H)
 504           ##]
 505  ##| ##26: ncases t2; nnormalize; #H;
 506           ##[ ##26: napply (refl_eq ??)
 507           ##| ##*: napply (bool_destruct ??? H)
 508           ##]
 509  ##| ##27: ncases t2; nnormalize; #H;
 510           ##[ ##27: napply (refl_eq ??)
 511           ##| ##*: napply (bool_destruct ??? H)
 512           ##]
 513  ##| ##28: ncases t2; nnormalize; #H;
 514           ##[ ##28: napply (refl_eq ??)
 515           ##| ##*: napply (bool_destruct ??? H)
 516           ##]
 517  ##| ##29: ncases t2; nnormalize; #H;
 518           ##[ ##29: napply (refl_eq ??)
 519           ##| ##*: napply (bool_destruct ??? H)
 520           ##]
 521  ##| ##30: ncases t2; nnormalize; #H;
 522           ##[ ##30: napply (refl_eq ??)
 523           ##| ##*: napply (bool_destruct ??? H)
 524           ##]
 525  ##| ##31: ncases t2; nnormalize; #H;
 526           ##[ ##31: napply (refl_eq ??)
 527           ##| ##*: napply (bool_destruct ??? H)
 528           ##]
 529  ##| ##32: ncases t2; nnormalize; #H;
 530           ##[ ##32: napply (refl_eq ??)
 531           ##| ##*: napply (bool_destruct ??? H)
 532           ##]
 533  ##]
 534 nqed.
 535
 536 nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
 537  #t1; #t2;
 538  ncases t1;
 539  ##[ ##1: ncases t2; nnormalize; #H;
 540           ##[ ##1: napply (refl_eq ??)
 541           ##| ##*: napply (bitrigesim_destruct ??? H)
 542           ##]
 543  ##| ##2: ncases t2; nnormalize; #H;
 544           ##[ ##2: napply (refl_eq ??)
 545           ##| ##*: napply (bitrigesim_destruct ??? H)
 546           ##]
 547  ##| ##3: ncases t2; nnormalize; #H;
 548           ##[ ##3: napply (refl_eq ??)
 549           ##| ##*: napply (bitrigesim_destruct ??? H)
 550           ##]
 551  ##| ##4: ncases t2; nnormalize; #H;
 552           ##[ ##4: napply (refl_eq ??)
 553           ##| ##*: napply (bitrigesim_destruct ??? H)
 554           ##]
 555  ##| ##5: ncases t2; nnormalize; #H;
 556           ##[ ##5: napply (refl_eq ??)
 557           ##| ##*: napply (bitrigesim_destruct ??? H)
 558           ##]
 559  ##| ##6: ncases t2; nnormalize; #H;
 560           ##[ ##6: napply (refl_eq ??)
 561           ##| ##*: napply (bitrigesim_destruct ??? H)
 562           ##]
 563  ##| ##7: ncases t2; nnormalize; #H;
 564           ##[ ##7: napply (refl_eq ??)
 565           ##| ##*: napply (bitrigesim_destruct ??? H)
 566           ##]
 567  ##| ##8: ncases t2; nnormalize; #H;
 568           ##[ ##8: napply (refl_eq ??)
 569           ##| ##*: napply (bitrigesim_destruct ??? H)
 570           ##]
 571  ##| ##9: ncases t2; nnormalize; #H;
 572           ##[ ##9: napply (refl_eq ??)
 573           ##| ##*: napply (bitrigesim_destruct ??? H)
 574           ##]
 575  ##| ##10: ncases t2; nnormalize; #H;
 576           ##[ ##10: napply (refl_eq ??)
 577           ##| ##*: napply (bitrigesim_destruct ??? H)
 578           ##]
 579  ##| ##11: ncases t2; nnormalize; #H;
 580           ##[ ##11: napply (refl_eq ??)
 581           ##| ##*: napply (bitrigesim_destruct ??? H)
 582           ##]
 583  ##| ##12: ncases t2; nnormalize; #H;
 584           ##[ ##12: napply (refl_eq ??)
 585           ##| ##*: napply (bitrigesim_destruct ??? H)
 586           ##]
 587  ##| ##13: ncases t2; nnormalize; #H;
 588           ##[ ##13: napply (refl_eq ??)
 589           ##| ##*: napply (bitrigesim_destruct ??? H)
 590           ##]
 591  ##| ##14: ncases t2; nnormalize; #H;
 592           ##[ ##14: napply (refl_eq ??)
 593           ##| ##*: napply (bitrigesim_destruct ??? H)
 594           ##]
 595  ##| ##15: ncases t2; nnormalize; #H;
 596           ##[ ##15: napply (refl_eq ??)
 597           ##| ##*: napply (bitrigesim_destruct ??? H)
 598           ##]
 599  ##| ##16: ncases t2; nnormalize; #H;
 600           ##[ ##16: napply (refl_eq ??)
 601           ##| ##*: napply (bitrigesim_destruct ??? H)
 602           ##]
 603  ##| ##17: ncases t2; nnormalize; #H;
 604           ##[ ##17: napply (refl_eq ??)
 605           ##| ##*: napply (bitrigesim_destruct ??? H)
 606           ##]
 607  ##| ##18: ncases t2; nnormalize; #H;
 608           ##[ ##18: napply (refl_eq ??)
 609           ##| ##*: napply (bitrigesim_destruct ??? H)
 610           ##]
 611  ##| ##19: ncases t2; nnormalize; #H;
 612           ##[ ##19: napply (refl_eq ??)
 613           ##| ##*: napply (bitrigesim_destruct ??? H)
 614           ##]
 615  ##| ##20: ncases t2; nnormalize; #H;
 616           ##[ ##20: napply (refl_eq ??)
 617           ##| ##*: napply (bitrigesim_destruct ??? H)
 618           ##]
 619  ##| ##21: ncases t2; nnormalize; #H;
 620           ##[ ##21: napply (refl_eq ??)
 621           ##| ##*: napply (bitrigesim_destruct ??? H)
 622           ##]
 623  ##| ##22: ncases t2; nnormalize; #H;
 624           ##[ ##22: napply (refl_eq ??)
 625           ##| ##*: napply (bitrigesim_destruct ??? H)
 626           ##]
 627  ##| ##23: ncases t2; nnormalize; #H;
 628           ##[ ##23: napply (refl_eq ??)
 629           ##| ##*: napply (bitrigesim_destruct ??? H)
 630           ##]
 631  ##| ##24: ncases t2; nnormalize; #H;
 632           ##[ ##24: napply (refl_eq ??)
 633           ##| ##*: napply (bitrigesim_destruct ??? H)
 634           ##]
 635  ##| ##25: ncases t2; nnormalize; #H;
 636           ##[ ##25: napply (refl_eq ??)
 637           ##| ##*: napply (bitrigesim_destruct ??? H)
 638           ##]
 639  ##| ##26: ncases t2; nnormalize; #H;
 640           ##[ ##26: napply (refl_eq ??)
 641           ##| ##*: napply (bitrigesim_destruct ??? H)
 642           ##]
 643  ##| ##27: ncases t2; nnormalize; #H;
 644           ##[ ##27: napply (refl_eq ??)
 645           ##| ##*: napply (bitrigesim_destruct ??? H)
 646           ##]
 647  ##| ##28: ncases t2; nnormalize; #H;
 648           ##[ ##28: napply (refl_eq ??)
 649           ##| ##*: napply (bitrigesim_destruct ??? H)
 650           ##]
 651  ##| ##29: ncases t2; nnormalize; #H;
 652           ##[ ##29: napply (refl_eq ??)
 653           ##| ##*: napply (bitrigesim_destruct ??? H)
 654           ##]
 655  ##| ##30: ncases t2; nnormalize; #H;
 656           ##[ ##30: napply (refl_eq ??)
 657           ##| ##*: napply (bitrigesim_destruct ??? H)
 658           ##]
 659  ##| ##31: ncases t2; nnormalize; #H;
 660           ##[ ##31: napply (refl_eq ??)
 661           ##| ##*: napply (bitrigesim_destruct ??? H)
 662           ##]
 663  ##| ##32: ncases t2; nnormalize; #H;
 664           ##[ ##32: napply (refl_eq ??)
 665           ##| ##*: napply (bitrigesim_destruct ??? H)
 666           ##]
 667  ##]
 668 nqed.