helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.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 "common/ascii_lemmas1.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************************** *)
  27 (* DEFINIZIONE ASCII MINIMALE *)
  28 (* ************************** *)
  29
  30 nlemma decidable_ascii1 : ∀x:ascii.decidable (ch_0 = x).
  31  #x; nnormalize; nelim x;
  32  ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  33  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  34  ##]
  35 nqed.
  36
  37 nlemma decidable_ascii2 : ∀x:ascii.decidable (ch_1 = x).
  38  #x; nnormalize; nelim x;
  39  ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  40  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  41  ##]
  42 nqed.
  43
  44 nlemma decidable_ascii3 : ∀x:ascii.decidable (ch_2 = x).
  45  #x; nnormalize; nelim x;
  46  ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  47  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  48  ##]
  49 nqed.
  50
  51 nlemma decidable_ascii4 : ∀x:ascii.decidable (ch_3 = x).
  52  #x; nnormalize; nelim x;
  53  ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  54  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  55  ##]
  56 nqed.
  57
  58 nlemma decidable_ascii5 : ∀x:ascii.decidable (ch_4 = x).
  59  #x; nnormalize; nelim x;
  60  ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  61  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  62  ##]
  63 nqed.
  64
  65 nlemma decidable_ascii6 : ∀x:ascii.decidable (ch_5 = x).
  66  #x; nnormalize; nelim x;
  67  ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  68  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  69  ##]
  70 nqed.
  71
  72 nlemma decidable_ascii7 : ∀x:ascii.decidable (ch_6 = x).
  73  #x; nnormalize; nelim x;
  74  ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  75  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  76  ##]
  77 nqed.
  78
  79 nlemma decidable_ascii8 : ∀x:ascii.decidable (ch_7 = x).
  80  #x; nnormalize; nelim x;
  81  ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  82  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  83  ##]
  84 nqed.
  85
  86 nlemma decidable_ascii9 : ∀x:ascii.decidable (ch_8 = x).
  87  #x; nnormalize; nelim x;
  88  ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  89  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  90  ##]
  91 nqed.
  92
  93 nlemma decidable_ascii10 : ∀x:ascii.decidable (ch_9 = x).
  94  #x; nnormalize; nelim x;
  95  ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
  96  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
  97  ##]
  98 nqed.
  99
 100 nlemma decidable_ascii11 : ∀x:ascii.decidable (ch__ = x).
 101  #x; nnormalize; nelim x;
 102  ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 103  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 104  ##]
 105 nqed.
 106
 107 nlemma decidable_ascii12 : ∀x:ascii.decidable (ch_A = x).
 108  #x; nnormalize; nelim x;
 109  ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 110  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 111  ##]
 112 nqed.
 113
 114 nlemma decidable_ascii13 : ∀x:ascii.decidable (ch_B = x).
 115  #x; nnormalize; nelim x;
 116  ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 117  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 118  ##]
 119 nqed.
 120
 121 nlemma decidable_ascii14 : ∀x:ascii.decidable (ch_C = x).
 122  #x; nnormalize; nelim x;
 123  ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 124  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 125  ##]
 126 nqed.
 127
 128 nlemma decidable_ascii15 : ∀x:ascii.decidable (ch_D = x).
 129  #x; nnormalize; nelim x;
 130  ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 131  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 132  ##]
 133 nqed.
 134
 135 nlemma decidable_ascii16 : ∀x:ascii.decidable (ch_E = x).
 136  #x; nnormalize; nelim x;
 137  ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 138  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 139  ##]
 140 nqed.
 141
 142 nlemma decidable_ascii17 : ∀x:ascii.decidable (ch_F = x).
 143  #x; nnormalize; nelim x;
 144  ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 145  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 146  ##]
 147 nqed.
 148
 149 nlemma decidable_ascii18 : ∀x:ascii.decidable (ch_G = x).
 150  #x; nnormalize; nelim x;
 151  ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 152  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 153  ##]
 154 nqed.
 155
 156 nlemma decidable_ascii19 : ∀x:ascii.decidable (ch_H = x).
 157  #x; nnormalize; nelim x;
 158  ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 159  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 160  ##]
 161 nqed.
 162
 163 nlemma decidable_ascii20 : ∀x:ascii.decidable (ch_I = x).
 164  #x; nnormalize; nelim x;
 165  ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 166  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 167  ##]
 168 nqed.
 169
 170 nlemma decidable_ascii21 : ∀x:ascii.decidable (ch_J = x).
 171  #x; nnormalize; nelim x;
 172  ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 173  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 174  ##]
 175 nqed.
 176
 177 nlemma decidable_ascii22 : ∀x:ascii.decidable (ch_K = x).
 178  #x; nnormalize; nelim x;
 179  ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 180  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 181  ##]
 182 nqed.
 183
 184 nlemma decidable_ascii23 : ∀x:ascii.decidable (ch_L = x).
 185  #x; nnormalize; nelim x;
 186  ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 187  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 188  ##]
 189 nqed.
 190
 191 nlemma decidable_ascii24 : ∀x:ascii.decidable (ch_M = x).
 192  #x; nnormalize; nelim x;
 193  ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 194  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 195  ##]
 196 nqed.
 197
 198 nlemma decidable_ascii25 : ∀x:ascii.decidable (ch_N = x).
 199  #x; nnormalize; nelim x;
 200  ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 201  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 202  ##]
 203 nqed.
 204
 205 nlemma decidable_ascii26 : ∀x:ascii.decidable (ch_O = x).
 206  #x; nnormalize; nelim x;
 207  ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 208  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 209  ##]
 210 nqed.
 211
 212 nlemma decidable_ascii27 : ∀x:ascii.decidable (ch_P = x).
 213  #x; nnormalize; nelim x;
 214  ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 215  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 216  ##]
 217 nqed.
 218
 219 nlemma decidable_ascii28 : ∀x:ascii.decidable (ch_Q = x).
 220  #x; nnormalize; nelim x;
 221  ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 222  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 223  ##]
 224 nqed.
 225
 226 nlemma decidable_ascii29 : ∀x:ascii.decidable (ch_R = x).
 227  #x; nnormalize; nelim x;
 228  ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 229  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 230  ##]
 231 nqed.
 232
 233 nlemma decidable_ascii30 : ∀x:ascii.decidable (ch_S = x).
 234  #x; nnormalize; nelim x;
 235  ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 236  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 237  ##]
 238 nqed.
 239
 240 nlemma decidable_ascii31 : ∀x:ascii.decidable (ch_T = x).
 241  #x; nnormalize; nelim x;
 242  ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 243  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 244  ##]
 245 nqed.
 246
 247 nlemma decidable_ascii32 : ∀x:ascii.decidable (ch_U = x).
 248  #x; nnormalize; nelim x;
 249  ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 250  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 251  ##]
 252 nqed.
 253
 254 nlemma decidable_ascii33 : ∀x:ascii.decidable (ch_V = x).
 255  #x; nnormalize; nelim x;
 256  ##[ ##33: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 257  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 258  ##]
 259 nqed.
 260
 261 nlemma decidable_ascii34 : ∀x:ascii.decidable (ch_W = x).
 262  #x; nnormalize; nelim x;
 263  ##[ ##34: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 264  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 265  ##]
 266 nqed.
 267
 268 nlemma decidable_ascii35 : ∀x:ascii.decidable (ch_X = x).
 269  #x; nnormalize; nelim x;
 270  ##[ ##35: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 271  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 272  ##]
 273 nqed.
 274
 275 nlemma decidable_ascii36 : ∀x:ascii.decidable (ch_Y = x).
 276  #x; nnormalize; nelim x;
 277  ##[ ##36: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 278  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 279  ##]
 280 nqed.
 281
 282 nlemma decidable_ascii37 : ∀x:ascii.decidable (ch_Z = x).
 283  #x; nnormalize; nelim x;
 284  ##[ ##37: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 285  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 286  ##]
 287 nqed.
 288
 289 nlemma decidable_ascii38 : ∀x:ascii.decidable (ch_a = x).
 290  #x; nnormalize; nelim x;
 291  ##[ ##38: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 292  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 293  ##]
 294 nqed.
 295
 296 nlemma decidable_ascii39 : ∀x:ascii.decidable (ch_b = x).
 297  #x; nnormalize; nelim x;
 298  ##[ ##39: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 299  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 300  ##]
 301 nqed.
 302
 303 nlemma decidable_ascii40 : ∀x:ascii.decidable (ch_c = x).
 304  #x; nnormalize; nelim x;
 305  ##[ ##40: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 306  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 307  ##]
 308 nqed.
 309
 310 nlemma decidable_ascii41 : ∀x:ascii.decidable (ch_d = x).
 311  #x; nnormalize; nelim x;
 312  ##[ ##41: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 313  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 314  ##]
 315 nqed.
 316
 317 nlemma decidable_ascii42 : ∀x:ascii.decidable (ch_e = x).
 318  #x; nnormalize; nelim x;
 319  ##[ ##42: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 320  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 321  ##]
 322 nqed.
 323
 324 nlemma decidable_ascii43 : ∀x:ascii.decidable (ch_f = x).
 325  #x; nnormalize; nelim x;
 326  ##[ ##43: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 327  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 328  ##]
 329 nqed.
 330
 331 nlemma decidable_ascii44 : ∀x:ascii.decidable (ch_g = x).
 332  #x; nnormalize; nelim x;
 333  ##[ ##44: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 334  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 335  ##]
 336 nqed.
 337
 338 nlemma decidable_ascii45 : ∀x:ascii.decidable (ch_h = x).
 339  #x; nnormalize; nelim x;
 340  ##[ ##45: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 341  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 342  ##]
 343 nqed.
 344
 345 nlemma decidable_ascii46 : ∀x:ascii.decidable (ch_i = x).
 346  #x; nnormalize; nelim x;
 347  ##[ ##46: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 348  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 349  ##]
 350 nqed.
 351
 352 nlemma decidable_ascii47 : ∀x:ascii.decidable (ch_j = x).
 353  #x; nnormalize; nelim x;
 354  ##[ ##47: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 355  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 356  ##]
 357 nqed.
 358
 359 nlemma decidable_ascii48 : ∀x:ascii.decidable (ch_k = x).
 360  #x; nnormalize; nelim x;
 361  ##[ ##48: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 362  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 363  ##]
 364 nqed.
 365
 366 nlemma decidable_ascii49 : ∀x:ascii.decidable (ch_l = x).
 367  #x; nnormalize; nelim x;
 368  ##[ ##49: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 369  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 370  ##]
 371 nqed.
 372
 373 nlemma decidable_ascii50 : ∀x:ascii.decidable (ch_m = x).
 374  #x; nnormalize; nelim x;
 375  ##[ ##50: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 376  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 377  ##]
 378 nqed.
 379
 380 nlemma decidable_ascii51 : ∀x:ascii.decidable (ch_n = x).
 381  #x; nnormalize; nelim x;
 382  ##[ ##51: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 383  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 384  ##]
 385 nqed.
 386
 387 nlemma decidable_ascii52 : ∀x:ascii.decidable (ch_o = x).
 388  #x; nnormalize; nelim x;
 389  ##[ ##52: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 390  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 391  ##]
 392 nqed.
 393
 394 nlemma decidable_ascii53 : ∀x:ascii.decidable (ch_p = x).
 395  #x; nnormalize; nelim x;
 396  ##[ ##53: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 397  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 398  ##]
 399 nqed.
 400
 401 nlemma decidable_ascii54 : ∀x:ascii.decidable (ch_q = x).
 402  #x; nnormalize; nelim x;
 403  ##[ ##54: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 404  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 405  ##]
 406 nqed.
 407
 408 nlemma decidable_ascii55 : ∀x:ascii.decidable (ch_r = x).
 409  #x; nnormalize; nelim x;
 410  ##[ ##55: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 411  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 412  ##]
 413 nqed.
 414
 415 nlemma decidable_ascii56 : ∀x:ascii.decidable (ch_s = x).
 416  #x; nnormalize; nelim x;
 417  ##[ ##56: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 418  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 419  ##]
 420 nqed.
 421
 422 nlemma decidable_ascii57 : ∀x:ascii.decidable (ch_t = x).
 423  #x; nnormalize; nelim x;
 424  ##[ ##57: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 425  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 426  ##]
 427 nqed.
 428
 429 nlemma decidable_ascii58 : ∀x:ascii.decidable (ch_u = x).
 430  #x; nnormalize; nelim x;
 431  ##[ ##58: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 432  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 433  ##]
 434 nqed.
 435
 436 nlemma decidable_ascii59 : ∀x:ascii.decidable (ch_v = x).
 437  #x; nnormalize; nelim x;
 438  ##[ ##59: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 439  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 440  ##]
 441 nqed.
 442
 443 nlemma decidable_ascii60 : ∀x:ascii.decidable (ch_w = x).
 444  #x; nnormalize; nelim x;
 445  ##[ ##60: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 446  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 447  ##]
 448 nqed.
 449
 450 nlemma decidable_ascii61 : ∀x:ascii.decidable (ch_x = x).
 451  #x; nnormalize; nelim x;
 452  ##[ ##61: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 453  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 454  ##]
 455 nqed.
 456
 457 nlemma decidable_ascii62 : ∀x:ascii.decidable (ch_y = x).
 458  #x; nnormalize; nelim x;
 459  ##[ ##62: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 460  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 461  ##]
 462 nqed.
 463
 464 nlemma decidable_ascii63 : ∀x:ascii.decidable (ch_z = x).
 465  #x; nnormalize; nelim x;
 466  ##[ ##63: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 467  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
 468  ##]
 469 nqed.
 470
 471 nlemma decidable_ascii : ∀x,y:ascii.decidable (x = y).
 472  #a1; ncases a1;
 473  ##[ ##1: napply decidable_ascii1 ##| ##2: napply decidable_ascii2
 474  ##| ##3: napply decidable_ascii3 ##| ##4: napply decidable_ascii4
 475  ##| ##5: napply decidable_ascii5 ##| ##6: napply decidable_ascii6
 476  ##| ##7: napply decidable_ascii7 ##| ##8: napply decidable_ascii8
 477  ##| ##9: napply decidable_ascii9 ##| ##10: napply decidable_ascii10
 478  ##| ##11: napply decidable_ascii11 ##| ##12: napply decidable_ascii12
 479  ##| ##13: napply decidable_ascii13 ##| ##14: napply decidable_ascii14
 480  ##| ##15: napply decidable_ascii15 ##| ##16: napply decidable_ascii16
 481  ##| ##17: napply decidable_ascii17 ##| ##18: napply decidable_ascii18
 482  ##| ##19: napply decidable_ascii19 ##| ##20: napply decidable_ascii20
 483  ##| ##21: napply decidable_ascii21 ##| ##22: napply decidable_ascii22
 484  ##| ##23: napply decidable_ascii23 ##| ##24: napply decidable_ascii24
 485  ##| ##25: napply decidable_ascii25 ##| ##26: napply decidable_ascii26
 486  ##| ##27: napply decidable_ascii27 ##| ##28: napply decidable_ascii28
 487  ##| ##29: napply decidable_ascii29 ##| ##30: napply decidable_ascii30
 488  ##| ##31: napply decidable_ascii31 ##| ##32: napply decidable_ascii32
 489  ##| ##33: napply decidable_ascii33 ##| ##34: napply decidable_ascii34
 490  ##| ##35: napply decidable_ascii35 ##| ##36: napply decidable_ascii36
 491  ##| ##37: napply decidable_ascii37 ##| ##38: napply decidable_ascii38
 492  ##| ##39: napply decidable_ascii39 ##| ##40: napply decidable_ascii40
 493  ##| ##41: napply decidable_ascii41 ##| ##42: napply decidable_ascii42
 494  ##| ##43: napply decidable_ascii43 ##| ##44: napply decidable_ascii44
 495  ##| ##45: napply decidable_ascii45 ##| ##46: napply decidable_ascii46
 496  ##| ##47: napply decidable_ascii47 ##| ##48: napply decidable_ascii48
 497  ##| ##49: napply decidable_ascii49 ##| ##50: napply decidable_ascii50
 498  ##| ##51: napply decidable_ascii51 ##| ##52: napply decidable_ascii52
 499  ##| ##53: napply decidable_ascii53 ##| ##54: napply decidable_ascii54
 500  ##| ##55: napply decidable_ascii55 ##| ##56: napply decidable_ascii56
 501  ##| ##57: napply decidable_ascii57 ##| ##58: napply decidable_ascii58
 502  ##| ##59: napply decidable_ascii59 ##| ##60: napply decidable_ascii60
 503  ##| ##61: napply decidable_ascii61 ##| ##62: napply decidable_ascii62
 504  ##| ##63: napply decidable_ascii63 ##]
 505 nqed.