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