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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/bitrigesim.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************* *)
  27 (* BITRIGESIMALI *)
  28 (* ************* *)
  29
  30 ndefinition bitrigesim_destruct_aux ≝
  31 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
  32  match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
  33
  34 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
  35  #t1; #t2; #P; #H;
  36  nrewrite < H;
  37  nelim t1;
  38  nnormalize;
  39  napply (λx.x).
  40 nqed.
  41
  42 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
  43  #t1;
  44  nelim t1;
  45  ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
  46  ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
  47  ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
  48  ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
  49  ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
  50  ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
  51  ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
  52  ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
  53  ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
  54  ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
  55  ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
  56  ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
  57  ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
  58  ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
  59  ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
  60  ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
  61  ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
  62  ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
  63  ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
  64  ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
  65  ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
  66  ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
  67  ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
  68  ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
  69  ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
  70  ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
  71  ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
  72  ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
  73  ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
  74  ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
  75  ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
  76  ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
  77  ##]
  78 nqed.
  79
  80 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
  81  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
  82 nqed.
  83
  84 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
  85  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
  86 nqed.
  87
  88 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
  89  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
  90 nqed.
  91
  92 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
  93  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
  94 nqed.
  95
  96 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
  97  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
  98 nqed.
  99
 100 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
 101  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 102 nqed.
 103
 104 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
 105  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 106 nqed.
 107
 108 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
 109  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 110 nqed.
 111
 112 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
 113  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 114 nqed.
 115
 116 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
 117  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 118 nqed.
 119
 120 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
 121  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 122 nqed.
 123
 124 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
 125  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 126 nqed.
 127
 128 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
 129  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 130 nqed.
 131
 132 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
 133  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 134 nqed.
 135
 136 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
 137  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 138 nqed.
 139
 140 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
 141  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 142 nqed.
 143
 144 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
 145  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 146 nqed.
 147
 148 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
 149  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 150 nqed.
 151
 152 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
 153  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 154 nqed.
 155
 156 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
 157  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 158 nqed.
 159
 160 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
 161  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 162 nqed.
 163
 164 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
 165  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 166 nqed.
 167
 168 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
 169  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 170 nqed.
 171
 172 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
 173  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 174 nqed.
 175
 176 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
 177  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 178 nqed.
 179
 180 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
 181  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 182 nqed.
 183
 184 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
 185  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 186 nqed.
 187
 188 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
 189  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 190 nqed.
 191
 192 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
 193  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 194 nqed.
 195
 196 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
 197  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 198 nqed.
 199
 200 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
 201  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 202 nqed.
 203
 204 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
 205  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
 206 nqed.
 207
 208 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
 209  #t1; ncases t1;
 210  ##[ ##1: napply eqbit_to_eq1 ##| ##2: napply eqbit_to_eq2
 211  ##| ##3: napply eqbit_to_eq3 ##| ##4: napply eqbit_to_eq4
 212  ##| ##5: napply eqbit_to_eq5 ##| ##6: napply eqbit_to_eq6
 213  ##| ##7: napply eqbit_to_eq7 ##| ##8: napply eqbit_to_eq8
 214  ##| ##9: napply eqbit_to_eq9 ##| ##10: napply eqbit_to_eq10
 215  ##| ##11: napply eqbit_to_eq11 ##| ##12: napply eqbit_to_eq12
 216  ##| ##13: napply eqbit_to_eq13 ##| ##14: napply eqbit_to_eq14
 217  ##| ##15: napply eqbit_to_eq15 ##| ##16: napply eqbit_to_eq16
 218  ##| ##17: napply eqbit_to_eq17 ##| ##18: napply eqbit_to_eq18
 219  ##| ##19: napply eqbit_to_eq19 ##| ##20: napply eqbit_to_eq20
 220  ##| ##21: napply eqbit_to_eq21 ##| ##22: napply eqbit_to_eq22
 221  ##| ##23: napply eqbit_to_eq23 ##| ##24: napply eqbit_to_eq24
 222  ##| ##25: napply eqbit_to_eq25 ##| ##26: napply eqbit_to_eq26
 223  ##| ##27: napply eqbit_to_eq27 ##| ##28: napply eqbit_to_eq28
 224  ##| ##29: napply eqbit_to_eq29 ##| ##30: napply eqbit_to_eq30
 225  ##| ##31: napply eqbit_to_eq31 ##| ##32: napply eqbit_to_eq32
 226  ##]
 227 nqed.
 228
 229 nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
 230  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 231 nqed.
 232
 233 nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
 234  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 235 nqed.
 236
 237 nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
 238  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 239 nqed.
 240
 241 nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
 242  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 243 nqed.
 244
 245 nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
 246  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 247 nqed.
 248
 249 nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
 250  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 251 nqed.
 252
 253 nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
 254  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 255 nqed.
 256
 257 nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
 258  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 259 nqed.
 260
 261 nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
 262  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 263 nqed.
 264
 265 nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
 266  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 267 nqed.
 268
 269 nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
 270  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 271 nqed.
 272
 273 nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
 274  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 275 nqed.
 276
 277 nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
 278  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 279 nqed.
 280
 281 nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
 282  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 283 nqed.
 284
 285 nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
 286  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 287 nqed.
 288
 289 nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
 290  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 291 nqed.
 292
 293 nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
 294  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 295 nqed.
 296
 297 nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
 298  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 299 nqed.
 300
 301 nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
 302  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 303 nqed.
 304
 305 nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
 306  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 307 nqed.
 308
 309 nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
 310  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 311 nqed.
 312
 313 nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
 314  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 315 nqed.
 316
 317 nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
 318  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 319 nqed.
 320
 321 nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
 322  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 323 nqed.
 324
 325 nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
 326  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 327 nqed.
 328
 329 nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
 330  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 331 nqed.
 332
 333 nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
 334  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 335 nqed.
 336
 337 nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
 338  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 339 nqed.
 340
 341 nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
 342  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 343 nqed.
 344
 345 nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
 346  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 347 nqed.
 348
 349 nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
 350  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 351 nqed.
 352
 353 nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
 354  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
 355 nqed.
 356
 357 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
 358  #t1; ncases t1;
 359  ##[ ##1: napply eq_to_eqbit1 ##| ##2: napply eq_to_eqbit2
 360  ##| ##3: napply eq_to_eqbit3 ##| ##4: napply eq_to_eqbit4
 361  ##| ##5: napply eq_to_eqbit5 ##| ##6: napply eq_to_eqbit6
 362  ##| ##7: napply eq_to_eqbit7 ##| ##8: napply eq_to_eqbit8
 363  ##| ##9: napply eq_to_eqbit9 ##| ##10: napply eq_to_eqbit10
 364  ##| ##11: napply eq_to_eqbit11 ##| ##12: napply eq_to_eqbit12
 365  ##| ##13: napply eq_to_eqbit13 ##| ##14: napply eq_to_eqbit14
 366  ##| ##15: napply eq_to_eqbit15 ##| ##16: napply eq_to_eqbit16
 367  ##| ##17: napply eq_to_eqbit17 ##| ##18: napply eq_to_eqbit18
 368  ##| ##19: napply eq_to_eqbit19 ##| ##20: napply eq_to_eqbit20
 369  ##| ##21: napply eq_to_eqbit21 ##| ##22: napply eq_to_eqbit22
 370  ##| ##23: napply eq_to_eqbit23 ##| ##24: napply eq_to_eqbit24
 371  ##| ##25: napply eq_to_eqbit25 ##| ##26: napply eq_to_eqbit26
 372  ##| ##27: napply eq_to_eqbit27 ##| ##28: napply eq_to_eqbit28
 373  ##| ##29: napply eq_to_eqbit29 ##| ##30: napply eq_to_eqbit30
 374  ##| ##31: napply eq_to_eqbit31 ##| ##32: napply eq_to_eqbit32
 375  ##]
 376 nqed.
 377
 378 nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
 379  #x; nnormalize; nelim x;
 380  ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 381  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 382  ##]
 383 nqed.
 384
 385 nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
 386  #x; nnormalize; nelim x;
 387  ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 388  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 389  ##]
 390 nqed.
 391
 392 nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
 393  #x; nnormalize; nelim x;
 394  ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 395  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 396  ##]
 397 nqed.
 398
 399 nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
 400  #x; nnormalize; nelim x;
 401  ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 402  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 403  ##]
 404 nqed.
 405
 406 nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
 407  #x; nnormalize; nelim x;
 408  ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 409  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 410  ##]
 411 nqed.
 412
 413 nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
 414  #x; nnormalize; nelim x;
 415  ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 416  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 417  ##]
 418 nqed.
 419
 420 nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
 421  #x; nnormalize; nelim x;
 422  ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 423  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 424  ##]
 425 nqed.
 426
 427 nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
 428  #x; nnormalize; nelim x;
 429  ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 430  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 431  ##]
 432 nqed.
 433
 434 nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
 435  #x; nnormalize; nelim x;
 436  ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 437  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 438  ##]
 439 nqed.
 440
 441 nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
 442  #x; nnormalize; nelim x;
 443  ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 444  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 445  ##]
 446 nqed.
 447
 448 nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
 449  #x; nnormalize; nelim x;
 450  ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 451  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 452  ##]
 453 nqed.
 454
 455 nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
 456  #x; nnormalize; nelim x;
 457  ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 458  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 459  ##]
 460 nqed.
 461
 462 nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
 463  #x; nnormalize; nelim x;
 464  ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 465  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 466  ##]
 467 nqed.
 468
 469 nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
 470  #x; nnormalize; nelim x;
 471  ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 472  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 473  ##]
 474 nqed.
 475
 476 nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
 477  #x; nnormalize; nelim x;
 478  ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 479  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 480  ##]
 481 nqed.
 482
 483 nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
 484  #x; nnormalize; nelim x;
 485  ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 486  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 487  ##]
 488 nqed.
 489
 490 nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
 491  #x; nnormalize; nelim x;
 492  ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 493  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 494  ##]
 495 nqed.
 496
 497 nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
 498  #x; nnormalize; nelim x;
 499  ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 500  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 501  ##]
 502 nqed.
 503
 504 nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
 505  #x; nnormalize; nelim x;
 506  ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 507  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 508  ##]
 509 nqed.
 510
 511 nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
 512  #x; nnormalize; nelim x;
 513  ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 514  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 515  ##]
 516 nqed.
 517
 518 nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
 519  #x; nnormalize; nelim x;
 520  ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 521  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 522  ##]
 523 nqed.
 524
 525 nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
 526  #x; nnormalize; nelim x;
 527  ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 528  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 529  ##]
 530 nqed.
 531
 532 nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
 533  #x; nnormalize; nelim x;
 534  ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 535  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 536  ##]
 537 nqed.
 538
 539 nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
 540  #x; nnormalize; nelim x;
 541  ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 542  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 543  ##]
 544 nqed.
 545
 546 nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
 547  #x; nnormalize; nelim x;
 548  ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 549  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 550  ##]
 551 nqed.
 552
 553 nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
 554  #x; nnormalize; nelim x;
 555  ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 556  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 557  ##]
 558 nqed.
 559
 560 nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
 561  #x; nnormalize; nelim x;
 562  ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 563  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 564  ##]
 565 nqed.
 566
 567 nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
 568  #x; nnormalize; nelim x;
 569  ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 570  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 571  ##]
 572 nqed.
 573
 574 nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
 575  #x; nnormalize; nelim x;
 576  ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 577  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 578  ##]
 579 nqed.
 580
 581 nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
 582  #x; nnormalize; nelim x;
 583  ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 584  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 585  ##]
 586 nqed.
 587
 588 nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
 589  #x; nnormalize; nelim x;
 590  ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 591  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 592  ##]
 593 nqed.
 594
 595 nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
 596  #x; nnormalize; nelim x;
 597  ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 598  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
 599  ##]
 600 nqed.
 601
 602 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
 603  #x; nnormalize; nelim x;
 604  ##[ ##1: napply decidable_bit1 ##| ##2: napply decidable_bit2
 605  ##| ##3: napply decidable_bit3 ##| ##4: napply decidable_bit4
 606  ##| ##5: napply decidable_bit5 ##| ##6: napply decidable_bit6
 607  ##| ##7: napply decidable_bit7 ##| ##8: napply decidable_bit8
 608  ##| ##9: napply decidable_bit9 ##| ##10: napply decidable_bit10
 609  ##| ##11: napply decidable_bit11 ##| ##12: napply decidable_bit12
 610  ##| ##13: napply decidable_bit13 ##| ##14: napply decidable_bit14
 611  ##| ##15: napply decidable_bit15 ##| ##16: napply decidable_bit16
 612  ##| ##17: napply decidable_bit17 ##| ##18: napply decidable_bit18
 613  ##| ##19: napply decidable_bit19 ##| ##20: napply decidable_bit20
 614  ##| ##21: napply decidable_bit21 ##| ##22: napply decidable_bit22
 615  ##| ##23: napply decidable_bit23 ##| ##24: napply decidable_bit24
 616  ##| ##25: napply decidable_bit25 ##| ##26: napply decidable_bit26
 617  ##| ##27: napply decidable_bit27 ##| ##28: napply decidable_bit28
 618  ##| ##29: napply decidable_bit29 ##| ##30: napply decidable_bit30
 619  ##| ##31: napply decidable_bit31 ##| ##32: napply decidable_bit32
 620  ##]
 621 nqed.
 622
 623 nlemma neqbit_to_neq1 : ∀t2.eq_bit t00 t2 = false → t00 ≠ t2.
 624  #t2; ncases t2; nnormalize; #H;
 625  ##[ ##1: napply  (bool_destruct … H)
 626  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 627  ##]
 628 nqed.
 629
 630 nlemma neqbit_to_neq2 : ∀t2.eq_bit t01 t2 = false → t01 ≠ t2.
 631  #t2; ncases t2; nnormalize; #H;
 632  ##[ ##2: napply  (bool_destruct … H)
 633  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 634  ##]
 635 nqed.
 636
 637 nlemma neqbit_to_neq3 : ∀t2.eq_bit t02 t2 = false → t02 ≠ t2.
 638  #t2; ncases t2; nnormalize; #H;
 639  ##[ ##3: napply  (bool_destruct … H)
 640  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 641  ##]
 642 nqed.
 643
 644 nlemma neqbit_to_neq4 : ∀t2.eq_bit t03 t2 = false → t03 ≠ t2.
 645  #t2; ncases t2; nnormalize; #H;
 646  ##[ ##4: napply  (bool_destruct … H)
 647  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 648  ##]
 649 nqed.
 650
 651 nlemma neqbit_to_neq5 : ∀t2.eq_bit t04 t2 = false → t04 ≠ t2.
 652  #t2; ncases t2; nnormalize; #H;
 653  ##[ ##5: napply  (bool_destruct … H)
 654  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 655  ##]
 656 nqed.
 657
 658 nlemma neqbit_to_neq6 : ∀t2.eq_bit t05 t2 = false → t05 ≠ t2.
 659  #t2; ncases t2; nnormalize; #H;
 660  ##[ ##6: napply  (bool_destruct … H)
 661  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 662  ##]
 663 nqed.
 664
 665 nlemma neqbit_to_neq7 : ∀t2.eq_bit t06 t2 = false → t06 ≠ t2.
 666  #t2; ncases t2; nnormalize; #H;
 667  ##[ ##7: napply  (bool_destruct … H)
 668  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 669  ##]
 670 nqed.
 671
 672 nlemma neqbit_to_neq8 : ∀t2.eq_bit t07 t2 = false → t07 ≠ t2.
 673  #t2; ncases t2; nnormalize; #H;
 674  ##[ ##8: napply  (bool_destruct … H)
 675  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 676  ##]
 677 nqed.
 678
 679 nlemma neqbit_to_neq9 : ∀t2.eq_bit t08 t2 = false → t08 ≠ t2.
 680  #t2; ncases t2; nnormalize; #H;
 681  ##[ ##9: napply  (bool_destruct … H)
 682  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 683  ##]
 684 nqed.
 685
 686 nlemma neqbit_to_neq10 : ∀t2.eq_bit t09 t2 = false → t09 ≠ t2.
 687  #t2; ncases t2; nnormalize; #H;
 688  ##[ ##10: napply  (bool_destruct … H)
 689  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 690  ##]
 691 nqed.
 692
 693 nlemma neqbit_to_neq11 : ∀t2.eq_bit t0A t2 = false → t0A ≠ t2.
 694  #t2; ncases t2; nnormalize; #H;
 695  ##[ ##11: napply  (bool_destruct … H)
 696  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 697  ##]
 698 nqed.
 699
 700 nlemma neqbit_to_neq12 : ∀t2.eq_bit t0B t2 = false → t0B ≠ t2.
 701  #t2; ncases t2; nnormalize; #H;
 702  ##[ ##12: napply  (bool_destruct … H)
 703  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 704  ##]
 705 nqed.
 706
 707 nlemma neqbit_to_neq13 : ∀t2.eq_bit t0C t2 = false → t0C ≠ t2.
 708  #t2; ncases t2; nnormalize; #H;
 709  ##[ ##13: napply  (bool_destruct … H)
 710  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 711  ##]
 712 nqed.
 713
 714 nlemma neqbit_to_neq14 : ∀t2.eq_bit t0D t2 = false → t0D ≠ t2.
 715  #t2; ncases t2; nnormalize; #H;
 716  ##[ ##14: napply  (bool_destruct … H)
 717  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 718  ##]
 719 nqed.
 720
 721 nlemma neqbit_to_neq15 : ∀t2.eq_bit t0E t2 = false → t0E ≠ t2.
 722  #t2; ncases t2; nnormalize; #H;
 723  ##[ ##15: napply  (bool_destruct … H)
 724  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 725  ##]
 726 nqed.
 727
 728 nlemma neqbit_to_neq16 : ∀t2.eq_bit t0F t2 = false → t0F ≠ t2.
 729  #t2; ncases t2; nnormalize; #H;
 730  ##[ ##16: napply  (bool_destruct … H)
 731  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 732  ##]
 733 nqed.
 734
 735 nlemma neqbit_to_neq17 : ∀t2.eq_bit t10 t2 = false → t10 ≠ t2.
 736  #t2; ncases t2; nnormalize; #H;
 737  ##[ ##17: napply  (bool_destruct … H)
 738  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 739  ##]
 740 nqed.
 741
 742 nlemma neqbit_to_neq18 : ∀t2.eq_bit t11 t2 = false → t11 ≠ t2.
 743  #t2; ncases t2; nnormalize; #H;
 744  ##[ ##18: napply  (bool_destruct … H)
 745  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 746  ##]
 747 nqed.
 748
 749 nlemma neqbit_to_neq19 : ∀t2.eq_bit t12 t2 = false → t12 ≠ t2.
 750  #t2; ncases t2; nnormalize; #H;
 751  ##[ ##19: napply  (bool_destruct … H)
 752  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 753  ##]
 754 nqed.
 755
 756 nlemma neqbit_to_neq20 : ∀t2.eq_bit t13 t2 = false → t13 ≠ t2.
 757  #t2; ncases t2; nnormalize; #H;
 758  ##[ ##20: napply  (bool_destruct … H)
 759  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 760  ##]
 761 nqed.
 762
 763 nlemma neqbit_to_neq21 : ∀t2.eq_bit t14 t2 = false → t14 ≠ t2.
 764  #t2; ncases t2; nnormalize; #H;
 765  ##[ ##21: napply  (bool_destruct … H)
 766  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 767  ##]
 768 nqed.
 769
 770 nlemma neqbit_to_neq22 : ∀t2.eq_bit t15 t2 = false → t15 ≠ t2.
 771  #t2; ncases t2; nnormalize; #H;
 772  ##[ ##22: napply  (bool_destruct … H)
 773  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 774  ##]
 775 nqed.
 776
 777 nlemma neqbit_to_neq23 : ∀t2.eq_bit t16 t2 = false → t16 ≠ t2.
 778  #t2; ncases t2; nnormalize; #H;
 779  ##[ ##23: napply  (bool_destruct … H)
 780  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 781  ##]
 782 nqed.
 783
 784 nlemma neqbit_to_neq24 : ∀t2.eq_bit t17 t2 = false → t17 ≠ t2.
 785  #t2; ncases t2; nnormalize; #H;
 786  ##[ ##24: napply  (bool_destruct … H)
 787  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 788  ##]
 789 nqed.
 790
 791 nlemma neqbit_to_neq25 : ∀t2.eq_bit t18 t2 = false → t18 ≠ t2.
 792  #t2; ncases t2; nnormalize; #H;
 793  ##[ ##25: napply  (bool_destruct … H)
 794  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 795  ##]
 796 nqed.
 797
 798 nlemma neqbit_to_neq26 : ∀t2.eq_bit t19 t2 = false → t19 ≠ t2.
 799  #t2; ncases t2; nnormalize; #H;
 800  ##[ ##26: napply  (bool_destruct … H)
 801  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 802  ##]
 803 nqed.
 804
 805 nlemma neqbit_to_neq27 : ∀t2.eq_bit t1A t2 = false → t1A ≠ t2.
 806  #t2; ncases t2; nnormalize; #H;
 807  ##[ ##27: napply  (bool_destruct … H)
 808  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 809  ##]
 810 nqed.
 811
 812 nlemma neqbit_to_neq28 : ∀t2.eq_bit t1B t2 = false → t1B ≠ t2.
 813  #t2; ncases t2; nnormalize; #H;
 814  ##[ ##28: napply  (bool_destruct … H)
 815  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 816  ##]
 817 nqed.
 818
 819 nlemma neqbit_to_neq29 : ∀t2.eq_bit t1C t2 = false → t1C ≠ t2.
 820  #t2; ncases t2; nnormalize; #H;
 821  ##[ ##29: napply  (bool_destruct … H)
 822  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 823  ##]
 824 nqed.
 825
 826 nlemma neqbit_to_neq30 : ∀t2.eq_bit t1D t2 = false → t1D ≠ t2.
 827  #t2; ncases t2; nnormalize; #H;
 828  ##[ ##30: napply  (bool_destruct … H)
 829  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 830  ##]
 831 nqed.
 832
 833 nlemma neqbit_to_neq31 : ∀t2.eq_bit t1E t2 = false → t1E ≠ t2.
 834  #t2; ncases t2; nnormalize; #H;
 835  ##[ ##31: napply  (bool_destruct … H)
 836  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 837  ##]
 838 nqed.
 839
 840 nlemma neqbit_to_neq32 : ∀t2.eq_bit t1F t2 = false → t1F ≠ t2.
 841  #t2; ncases t2; nnormalize; #H;
 842  ##[ ##32: napply  (bool_destruct … H)
 843  ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
 844  ##]
 845 nqed.
 846
 847 nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
 848  #t1; nelim t1;
 849  ##[ ##1: napply neqbit_to_neq1 ##| ##2: napply neqbit_to_neq2
 850  ##| ##3: napply neqbit_to_neq3 ##| ##4: napply neqbit_to_neq4
 851  ##| ##5: napply neqbit_to_neq5 ##| ##6: napply neqbit_to_neq6
 852  ##| ##7: napply neqbit_to_neq7 ##| ##8: napply neqbit_to_neq8
 853  ##| ##9: napply neqbit_to_neq9 ##| ##10: napply neqbit_to_neq10
 854  ##| ##11: napply neqbit_to_neq11 ##| ##12: napply neqbit_to_neq12
 855  ##| ##13: napply neqbit_to_neq13 ##| ##14: napply neqbit_to_neq14
 856  ##| ##15: napply neqbit_to_neq15 ##| ##16: napply neqbit_to_neq16
 857  ##| ##17: napply neqbit_to_neq17 ##| ##18: napply neqbit_to_neq18
 858  ##| ##19: napply neqbit_to_neq19 ##| ##20: napply neqbit_to_neq20
 859  ##| ##21: napply neqbit_to_neq21 ##| ##22: napply neqbit_to_neq22
 860  ##| ##23: napply neqbit_to_neq23 ##| ##24: napply neqbit_to_neq24
 861  ##| ##25: napply neqbit_to_neq25 ##| ##26: napply neqbit_to_neq26
 862  ##| ##27: napply neqbit_to_neq27 ##| ##28: napply neqbit_to_neq28
 863  ##| ##29: napply neqbit_to_neq29 ##| ##30: napply neqbit_to_neq30
 864  ##| ##31: napply neqbit_to_neq31 ##| ##32: napply neqbit_to_neq32
 865  ##]
 866 nqed.
 867
 868 nlemma neq_to_neqbit1 : ∀t2.t00 ≠ t2 → eq_bit t00 t2 = false.
 869  #t2; ncases t2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 870 nqed.
 871
 872 nlemma neq_to_neqbit2 : ∀t2.t01 ≠ t2 → eq_bit t01 t2 = false.
 873  #t2; ncases t2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 874 nqed.
 875
 876 nlemma neq_to_neqbit3 : ∀t2.t02 ≠ t2 → eq_bit t02 t2 = false.
 877  #t2; ncases t2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 878 nqed.
 879
 880 nlemma neq_to_neqbit4 : ∀t2.t03 ≠ t2 → eq_bit t03 t2 = false.
 881  #t2; ncases t2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 882 nqed.
 883
 884 nlemma neq_to_neqbit5 : ∀t2.t04 ≠ t2 → eq_bit t04 t2 = false.
 885  #t2; ncases t2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 886 nqed.
 887
 888 nlemma neq_to_neqbit6 : ∀t2.t05 ≠ t2 → eq_bit t05 t2 = false.
 889  #t2; ncases t2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 890 nqed.
 891
 892 nlemma neq_to_neqbit7 : ∀t2.t06 ≠ t2 → eq_bit t06 t2 = false.
 893  #t2; ncases t2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 894 nqed.
 895
 896 nlemma neq_to_neqbit8 : ∀t2.t07 ≠ t2 → eq_bit t07 t2 = false.
 897  #t2; ncases t2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 898 nqed.
 899
 900 nlemma neq_to_neqbit9 : ∀t2.t08 ≠ t2 → eq_bit t08 t2 = false.
 901  #t2; ncases t2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 902 nqed.
 903
 904 nlemma neq_to_neqbit10 : ∀t2.t09 ≠ t2 → eq_bit t09 t2 = false.
 905  #t2; ncases t2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 906 nqed.
 907
 908 nlemma neq_to_neqbit11 : ∀t2.t0A ≠ t2 → eq_bit t0A t2 = false.
 909  #t2; ncases t2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 910 nqed.
 911
 912 nlemma neq_to_neqbit12 : ∀t2.t0B ≠ t2 → eq_bit t0B t2 = false.
 913  #t2; ncases t2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 914 nqed.
 915
 916 nlemma neq_to_neqbit13 : ∀t2.t0C ≠ t2 → eq_bit t0C t2 = false.
 917  #t2; ncases t2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 918 nqed.
 919
 920 nlemma neq_to_neqbit14 : ∀t2.t0D ≠ t2 → eq_bit t0D t2 = false.
 921  #t2; ncases t2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 922 nqed.
 923
 924 nlemma neq_to_neqbit15 : ∀t2.t0E ≠ t2 → eq_bit t0E t2 = false.
 925  #t2; ncases t2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 926 nqed.
 927
 928 nlemma neq_to_neqbit16 : ∀t2.t0F ≠ t2 → eq_bit t0F t2 = false.
 929  #t2; ncases t2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 930 nqed.
 931
 932 nlemma neq_to_neqbit17 : ∀t2.t10 ≠ t2 → eq_bit t10 t2 = false.
 933  #t2; ncases t2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 934 nqed.
 935
 936 nlemma neq_to_neqbit18 : ∀t2.t11 ≠ t2 → eq_bit t11 t2 = false.
 937  #t2; ncases t2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 938 nqed.
 939
 940 nlemma neq_to_neqbit19 : ∀t2.t12 ≠ t2 → eq_bit t12 t2 = false.
 941  #t2; ncases t2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 942 nqed.
 943
 944 nlemma neq_to_neqbit20 : ∀t2.t13 ≠ t2 → eq_bit t13 t2 = false.
 945  #t2; ncases t2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 946 nqed.
 947
 948 nlemma neq_to_neqbit21 : ∀t2.t14 ≠ t2 → eq_bit t14 t2 = false.
 949  #t2; ncases t2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 950 nqed.
 951
 952 nlemma neq_to_neqbit22 : ∀t2.t15 ≠ t2 → eq_bit t15 t2 = false.
 953  #t2; ncases t2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 954 nqed.
 955
 956 nlemma neq_to_neqbit23 : ∀t2.t16 ≠ t2 → eq_bit t16 t2 = false.
 957  #t2; ncases t2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 958 nqed.
 959
 960 nlemma neq_to_neqbit24 : ∀t2.t17 ≠ t2 → eq_bit t17 t2 = false.
 961  #t2; ncases t2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 962 nqed.
 963
 964 nlemma neq_to_neqbit25 : ∀t2.t18 ≠ t2 → eq_bit t18 t2 = false.
 965  #t2; ncases t2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 966 nqed.
 967
 968 nlemma neq_to_neqbit26 : ∀t2.t19 ≠ t2 → eq_bit t19 t2 = false.
 969  #t2; ncases t2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 970 nqed.
 971
 972 nlemma neq_to_neqbit27 : ∀t2.t1A ≠ t2 → eq_bit t1A t2 = false.
 973  #t2; ncases t2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 974 nqed.
 975
 976 nlemma neq_to_neqbit28 : ∀t2.t1B ≠ t2 → eq_bit t1B t2 = false.
 977  #t2; ncases t2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 978 nqed.
 979
 980 nlemma neq_to_neqbit29 : ∀t2.t1C ≠ t2 → eq_bit t1C t2 = false.
 981  #t2; ncases t2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 982 nqed.
 983
 984 nlemma neq_to_neqbit30 : ∀t2.t1D ≠ t2 → eq_bit t1D t2 = false.
 985  #t2; ncases t2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 986 nqed.
 987
 988 nlemma neq_to_neqbit31 : ∀t2.t1E ≠ t2 → eq_bit t1E t2 = false.
 989  #t2; ncases t2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 990 nqed.
 991
 992 nlemma neq_to_neqbit32 : ∀t2.t1F ≠ t2 → eq_bit t1F t2 = false.
 993  #t2; ncases t2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
 994 nqed.
 995
 996 nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
 997  #t1; nelim t1;
 998  ##[ ##1: napply neq_to_neqbit1 ##| ##2: napply neq_to_neqbit2
 999  ##| ##3: napply neq_to_neqbit3 ##| ##4: napply neq_to_neqbit4
1000  ##| ##5: napply neq_to_neqbit5 ##| ##6: napply neq_to_neqbit6
1001  ##| ##7: napply neq_to_neqbit7 ##| ##8: napply neq_to_neqbit8
1002  ##| ##9: napply neq_to_neqbit9 ##| ##10: napply neq_to_neqbit10
1003  ##| ##11: napply neq_to_neqbit11 ##| ##12: napply neq_to_neqbit12
1004  ##| ##13: napply neq_to_neqbit13 ##| ##14: napply neq_to_neqbit14
1005  ##| ##15: napply neq_to_neqbit15 ##| ##16: napply neq_to_neqbit16
1006  ##| ##17: napply neq_to_neqbit17 ##| ##18: napply neq_to_neqbit18
1007  ##| ##19: napply neq_to_neqbit19 ##| ##20: napply neq_to_neqbit20
1008  ##| ##21: napply neq_to_neqbit21 ##| ##22: napply neq_to_neqbit22
1009  ##| ##23: napply neq_to_neqbit23 ##| ##24: napply neq_to_neqbit24
1010  ##| ##25: napply neq_to_neqbit25 ##| ##26: napply neq_to_neqbit26
1011  ##| ##27: napply neq_to_neqbit27 ##| ##28: napply neq_to_neqbit28
1012  ##| ##29: napply neq_to_neqbit29 ##| ##30: napply neq_to_neqbit30
1013  ##| ##31: napply neq_to_neqbit31 ##| ##32: napply neq_to_neqbit32
1014  ##]
1015 nqed.