helm/software/matita/contribs/ng_assembly/common/ascii_lemmas4.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 neqascii_to_neq1 : ∀a2.eq_ascii ch_0 a2 = false → ch_0 ≠ a2.
  31  #a2; ncases a2; nnormalize; #H;
  32  ##[ ##1: napply  (bool_destruct … H)
  33  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  34  ##]
  35 nqed.
  36
  37 nlemma neqascii_to_neq2 : ∀a2.eq_ascii ch_1 a2 = false → ch_1 ≠ a2.
  38  #a2; ncases a2; nnormalize; #H;
  39  ##[ ##2: napply  (bool_destruct … H)
  40  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  41  ##]
  42 nqed.
  43
  44 nlemma neqascii_to_neq3 : ∀a2.eq_ascii ch_2 a2 = false → ch_2 ≠ a2.
  45  #a2; ncases a2; nnormalize; #H;
  46  ##[ ##3: napply  (bool_destruct … H)
  47  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  48  ##]
  49 nqed.
  50
  51 nlemma neqascii_to_neq4 : ∀a2.eq_ascii ch_3 a2 = false → ch_3 ≠ a2.
  52  #a2; ncases a2; nnormalize; #H;
  53  ##[ ##4: napply  (bool_destruct … H)
  54  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  55  ##]
  56 nqed.
  57
  58 nlemma neqascii_to_neq5 : ∀a2.eq_ascii ch_4 a2 = false → ch_4 ≠ a2.
  59  #a2; ncases a2; nnormalize; #H;
  60  ##[ ##5: napply  (bool_destruct … H)
  61  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  62  ##]
  63 nqed.
  64
  65 nlemma neqascii_to_neq6 : ∀a2.eq_ascii ch_5 a2 = false → ch_5 ≠ a2.
  66  #a2; ncases a2; nnormalize; #H;
  67  ##[ ##6: napply  (bool_destruct … H)
  68  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  69  ##]
  70 nqed.
  71
  72 nlemma neqascii_to_neq7 : ∀a2.eq_ascii ch_6 a2 = false → ch_6 ≠ a2.
  73  #a2; ncases a2; nnormalize; #H;
  74  ##[ ##7: napply  (bool_destruct … H)
  75  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  76  ##]
  77 nqed.
  78
  79 nlemma neqascii_to_neq8 : ∀a2.eq_ascii ch_7 a2 = false → ch_7 ≠ a2.
  80  #a2; ncases a2; nnormalize; #H;
  81  ##[ ##8: napply  (bool_destruct … H)
  82  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  83  ##]
  84 nqed.
  85
  86 nlemma neqascii_to_neq9 : ∀a2.eq_ascii ch_8 a2 = false → ch_8 ≠ a2.
  87  #a2; ncases a2; nnormalize; #H;
  88  ##[ ##9: napply  (bool_destruct … H)
  89  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  90  ##]
  91 nqed.
  92
  93 nlemma neqascii_to_neq10 : ∀a2.eq_ascii ch_9 a2 = false → ch_9 ≠ a2.
  94  #a2; ncases a2; nnormalize; #H;
  95  ##[ ##10: napply  (bool_destruct … H)
  96  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
  97  ##]
  98 nqed.
  99
 100 nlemma neqascii_to_neq11 : ∀a2.eq_ascii ch__ a2 = false → ch__ ≠ a2.
 101  #a2; ncases a2; nnormalize; #H;
 102  ##[ ##11: napply  (bool_destruct … H)
 103  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 104  ##]
 105 nqed.
 106
 107 nlemma neqascii_to_neq12 : ∀a2.eq_ascii ch_A a2 = false → ch_A ≠ a2.
 108  #a2; ncases a2; nnormalize; #H;
 109  ##[ ##12: napply  (bool_destruct … H)
 110  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 111  ##]
 112 nqed.
 113
 114 nlemma neqascii_to_neq13 : ∀a2.eq_ascii ch_B a2 = false → ch_B ≠ a2.
 115  #a2; ncases a2; nnormalize; #H;
 116  ##[ ##13: napply  (bool_destruct … H)
 117  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 118  ##]
 119 nqed.
 120
 121 nlemma neqascii_to_neq14 : ∀a2.eq_ascii ch_C a2 = false → ch_C ≠ a2.
 122  #a2; ncases a2; nnormalize; #H;
 123  ##[ ##14: napply  (bool_destruct … H)
 124  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 125  ##]
 126 nqed.
 127
 128 nlemma neqascii_to_neq15 : ∀a2.eq_ascii ch_D a2 = false → ch_D ≠ a2.
 129  #a2; ncases a2; nnormalize; #H;
 130  ##[ ##15: napply  (bool_destruct … H)
 131  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 132  ##]
 133 nqed.
 134
 135 nlemma neqascii_to_neq16 : ∀a2.eq_ascii ch_E a2 = false → ch_E ≠ a2.
 136  #a2; ncases a2; nnormalize; #H;
 137  ##[ ##16: napply  (bool_destruct … H)
 138  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 139  ##]
 140 nqed.
 141
 142 nlemma neqascii_to_neq17 : ∀a2.eq_ascii ch_F a2 = false → ch_F ≠ a2.
 143  #a2; ncases a2; nnormalize; #H;
 144  ##[ ##17: napply  (bool_destruct … H)
 145  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 146  ##]
 147 nqed.
 148
 149 nlemma neqascii_to_neq18 : ∀a2.eq_ascii ch_G a2 = false → ch_G ≠ a2.
 150  #a2; ncases a2; nnormalize; #H;
 151  ##[ ##18: napply  (bool_destruct … H)
 152  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 153  ##]
 154 nqed.
 155
 156 nlemma neqascii_to_neq19 : ∀a2.eq_ascii ch_H a2 = false → ch_H ≠ a2.
 157  #a2; ncases a2; nnormalize; #H;
 158  ##[ ##19: napply  (bool_destruct … H)
 159  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 160  ##]
 161 nqed.
 162
 163 nlemma neqascii_to_neq20 : ∀a2.eq_ascii ch_I a2 = false → ch_I ≠ a2.
 164  #a2; ncases a2; nnormalize; #H;
 165  ##[ ##20: napply  (bool_destruct … H)
 166  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 167  ##]
 168 nqed.
 169
 170 nlemma neqascii_to_neq21 : ∀a2.eq_ascii ch_J a2 = false → ch_J ≠ a2.
 171  #a2; ncases a2; nnormalize; #H;
 172  ##[ ##21: napply  (bool_destruct … H)
 173  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 174  ##]
 175 nqed.
 176
 177 nlemma neqascii_to_neq22 : ∀a2.eq_ascii ch_K a2 = false → ch_K ≠ a2.
 178  #a2; ncases a2; nnormalize; #H;
 179  ##[ ##22: napply  (bool_destruct … H)
 180  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 181  ##]
 182 nqed.
 183
 184 nlemma neqascii_to_neq23 : ∀a2.eq_ascii ch_L a2 = false → ch_L ≠ a2.
 185  #a2; ncases a2; nnormalize; #H;
 186  ##[ ##23: napply  (bool_destruct … H)
 187  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 188  ##]
 189 nqed.
 190
 191 nlemma neqascii_to_neq24 : ∀a2.eq_ascii ch_M a2 = false → ch_M ≠ a2.
 192  #a2; ncases a2; nnormalize; #H;
 193  ##[ ##24: napply  (bool_destruct … H)
 194  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 195  ##]
 196 nqed.
 197
 198 nlemma neqascii_to_neq25 : ∀a2.eq_ascii ch_N a2 = false → ch_N ≠ a2.
 199  #a2; ncases a2; nnormalize; #H;
 200  ##[ ##25: napply  (bool_destruct … H)
 201  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 202  ##]
 203 nqed.
 204
 205 nlemma neqascii_to_neq26 : ∀a2.eq_ascii ch_O a2 = false → ch_O ≠ a2.
 206  #a2; ncases a2; nnormalize; #H;
 207  ##[ ##26: napply  (bool_destruct … H)
 208  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 209  ##]
 210 nqed.
 211
 212 nlemma neqascii_to_neq27 : ∀a2.eq_ascii ch_P a2 = false → ch_P ≠ a2.
 213  #a2; ncases a2; nnormalize; #H;
 214  ##[ ##27: napply  (bool_destruct … H)
 215  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 216  ##]
 217 nqed.
 218
 219 nlemma neqascii_to_neq28 : ∀a2.eq_ascii ch_Q a2 = false → ch_Q ≠ a2.
 220  #a2; ncases a2; nnormalize; #H;
 221  ##[ ##28: napply  (bool_destruct … H)
 222  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 223  ##]
 224 nqed.
 225
 226 nlemma neqascii_to_neq29 : ∀a2.eq_ascii ch_R a2 = false → ch_R ≠ a2.
 227  #a2; ncases a2; nnormalize; #H;
 228  ##[ ##29: napply  (bool_destruct … H)
 229  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 230  ##]
 231 nqed.
 232
 233 nlemma neqascii_to_neq30 : ∀a2.eq_ascii ch_S a2 = false → ch_S ≠ a2.
 234  #a2; ncases a2; nnormalize; #H;
 235  ##[ ##30: napply  (bool_destruct … H)
 236  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 237  ##]
 238 nqed.
 239
 240 nlemma neqascii_to_neq31 : ∀a2.eq_ascii ch_T a2 = false → ch_T ≠ a2.
 241  #a2; ncases a2; nnormalize; #H;
 242  ##[ ##31: napply  (bool_destruct … H)
 243  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 244  ##]
 245 nqed.
 246
 247 nlemma neqascii_to_neq32 : ∀a2.eq_ascii ch_U a2 = false → ch_U ≠ a2.
 248  #a2; ncases a2; nnormalize; #H;
 249  ##[ ##32: napply  (bool_destruct … H)
 250  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 251  ##]
 252 nqed.
 253
 254 nlemma neqascii_to_neq33 : ∀a2.eq_ascii ch_V a2 = false → ch_V ≠ a2.
 255  #a2; ncases a2; nnormalize; #H;
 256  ##[ ##33: napply  (bool_destruct … H)
 257  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 258  ##]
 259 nqed.
 260
 261 nlemma neqascii_to_neq34 : ∀a2.eq_ascii ch_W a2 = false → ch_W ≠ a2.
 262  #a2; ncases a2; nnormalize; #H;
 263  ##[ ##34: napply  (bool_destruct … H)
 264  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 265  ##]
 266 nqed.
 267
 268 nlemma neqascii_to_neq35 : ∀a2.eq_ascii ch_X a2 = false → ch_X ≠ a2.
 269  #a2; ncases a2; nnormalize; #H;
 270  ##[ ##35: napply  (bool_destruct … H)
 271  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 272  ##]
 273 nqed.
 274
 275 nlemma neqascii_to_neq36 : ∀a2.eq_ascii ch_Y a2 = false → ch_Y ≠ a2.
 276  #a2; ncases a2; nnormalize; #H;
 277  ##[ ##36: napply  (bool_destruct … H)
 278  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 279  ##]
 280 nqed.
 281
 282 nlemma neqascii_to_neq37 : ∀a2.eq_ascii ch_Z a2 = false → ch_Z ≠ a2.
 283  #a2; ncases a2; nnormalize; #H;
 284  ##[ ##37: napply  (bool_destruct … H)
 285  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 286  ##]
 287 nqed.
 288
 289 nlemma neqascii_to_neq38 : ∀a2.eq_ascii ch_a a2 = false → ch_a ≠ a2.
 290  #a2; ncases a2; nnormalize; #H;
 291  ##[ ##38: napply  (bool_destruct … H)
 292  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 293  ##]
 294 nqed.
 295
 296 nlemma neqascii_to_neq39 : ∀a2.eq_ascii ch_b a2 = false → ch_b ≠ a2.
 297  #a2; ncases a2; nnormalize; #H;
 298  ##[ ##39: napply  (bool_destruct … H)
 299  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 300  ##]
 301 nqed.
 302
 303 nlemma neqascii_to_neq40 : ∀a2.eq_ascii ch_c a2 = false → ch_c ≠ a2.
 304  #a2; ncases a2; nnormalize; #H;
 305  ##[ ##40: napply  (bool_destruct … H)
 306  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 307  ##]
 308 nqed.
 309
 310 nlemma neqascii_to_neq41 : ∀a2.eq_ascii ch_d a2 = false → ch_d ≠ a2.
 311  #a2; ncases a2; nnormalize; #H;
 312  ##[ ##41: napply  (bool_destruct … H)
 313  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 314  ##]
 315 nqed.
 316
 317 nlemma neqascii_to_neq42 : ∀a2.eq_ascii ch_e a2 = false → ch_e ≠ a2.
 318  #a2; ncases a2; nnormalize; #H;
 319  ##[ ##42: napply  (bool_destruct … H)
 320  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 321  ##]
 322 nqed.
 323
 324 nlemma neqascii_to_neq43 : ∀a2.eq_ascii ch_f a2 = false → ch_f ≠ a2.
 325  #a2; ncases a2; nnormalize; #H;
 326  ##[ ##43: napply  (bool_destruct … H)
 327  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 328  ##]
 329 nqed.
 330
 331 nlemma neqascii_to_neq44 : ∀a2.eq_ascii ch_g a2 = false → ch_g ≠ a2.
 332  #a2; ncases a2; nnormalize; #H;
 333  ##[ ##44: napply  (bool_destruct … H)
 334  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 335  ##]
 336 nqed.
 337
 338 nlemma neqascii_to_neq45 : ∀a2.eq_ascii ch_h a2 = false → ch_h ≠ a2.
 339  #a2; ncases a2; nnormalize; #H;
 340  ##[ ##45: napply  (bool_destruct … H)
 341  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 342  ##]
 343 nqed.
 344
 345 nlemma neqascii_to_neq46 : ∀a2.eq_ascii ch_i a2 = false → ch_i ≠ a2.
 346  #a2; ncases a2; nnormalize; #H;
 347  ##[ ##46: napply  (bool_destruct … H)
 348  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 349  ##]
 350 nqed.
 351
 352 nlemma neqascii_to_neq47 : ∀a2.eq_ascii ch_j a2 = false → ch_j ≠ a2.
 353  #a2; ncases a2; nnormalize; #H;
 354  ##[ ##47: napply  (bool_destruct … H)
 355  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 356  ##]
 357 nqed.
 358
 359 nlemma neqascii_to_neq48 : ∀a2.eq_ascii ch_k a2 = false → ch_k ≠ a2.
 360  #a2; ncases a2; nnormalize; #H;
 361  ##[ ##48: napply  (bool_destruct … H)
 362  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 363  ##]
 364 nqed.
 365
 366 nlemma neqascii_to_neq49 : ∀a2.eq_ascii ch_l a2 = false → ch_l ≠ a2.
 367  #a2; ncases a2; nnormalize; #H;
 368  ##[ ##49: napply  (bool_destruct … H)
 369  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 370  ##]
 371 nqed.
 372
 373 nlemma neqascii_to_neq50 : ∀a2.eq_ascii ch_m a2 = false → ch_m ≠ a2.
 374  #a2; ncases a2; nnormalize; #H;
 375  ##[ ##50: napply  (bool_destruct … H)
 376  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 377  ##]
 378 nqed.
 379
 380 nlemma neqascii_to_neq51 : ∀a2.eq_ascii ch_n a2 = false → ch_n ≠ a2.
 381  #a2; ncases a2; nnormalize; #H;
 382  ##[ ##51: napply  (bool_destruct … H)
 383  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 384  ##]
 385 nqed.
 386
 387 nlemma neqascii_to_neq52 : ∀a2.eq_ascii ch_o a2 = false → ch_o ≠ a2.
 388  #a2; ncases a2; nnormalize; #H;
 389  ##[ ##52: napply  (bool_destruct … H)
 390  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 391  ##]
 392 nqed.
 393
 394 nlemma neqascii_to_neq53 : ∀a2.eq_ascii ch_p a2 = false → ch_p ≠ a2.
 395  #a2; ncases a2; nnormalize; #H;
 396  ##[ ##53: napply  (bool_destruct … H)
 397  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 398  ##]
 399 nqed.
 400
 401 nlemma neqascii_to_neq54 : ∀a2.eq_ascii ch_q a2 = false → ch_q ≠ a2.
 402  #a2; ncases a2; nnormalize; #H;
 403  ##[ ##54: napply  (bool_destruct … H)
 404  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 405  ##]
 406 nqed.
 407
 408 nlemma neqascii_to_neq55 : ∀a2.eq_ascii ch_r a2 = false → ch_r ≠ a2.
 409  #a2; ncases a2; nnormalize; #H;
 410  ##[ ##55: napply  (bool_destruct … H)
 411  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 412  ##]
 413 nqed.
 414
 415 nlemma neqascii_to_neq56 : ∀a2.eq_ascii ch_s a2 = false → ch_s ≠ a2.
 416  #a2; ncases a2; nnormalize; #H;
 417  ##[ ##56: napply  (bool_destruct … H)
 418  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 419  ##]
 420 nqed.
 421
 422 nlemma neqascii_to_neq57 : ∀a2.eq_ascii ch_t a2 = false → ch_t ≠ a2.
 423  #a2; ncases a2; nnormalize; #H;
 424  ##[ ##57: napply  (bool_destruct … H)
 425  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 426  ##]
 427 nqed.
 428
 429 nlemma neqascii_to_neq58 : ∀a2.eq_ascii ch_u a2 = false → ch_u ≠ a2.
 430  #a2; ncases a2; nnormalize; #H;
 431  ##[ ##58: napply  (bool_destruct … H)
 432  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 433  ##]
 434 nqed.
 435
 436 nlemma neqascii_to_neq59 : ∀a2.eq_ascii ch_v a2 = false → ch_v ≠ a2.
 437  #a2; ncases a2; nnormalize; #H;
 438  ##[ ##59: napply  (bool_destruct … H)
 439  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 440  ##]
 441 nqed.
 442
 443 nlemma neqascii_to_neq60 : ∀a2.eq_ascii ch_w a2 = false → ch_w ≠ a2.
 444  #a2; ncases a2; nnormalize; #H;
 445  ##[ ##60: napply  (bool_destruct … H)
 446  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 447  ##]
 448 nqed.
 449
 450 nlemma neqascii_to_neq61 : ∀a2.eq_ascii ch_x a2 = false → ch_x ≠ a2.
 451  #a2; ncases a2; nnormalize; #H;
 452  ##[ ##61: napply  (bool_destruct … H)
 453  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 454  ##]
 455 nqed.
 456
 457 nlemma neqascii_to_neq62 : ∀a2.eq_ascii ch_y a2 = false → ch_y ≠ a2.
 458  #a2; ncases a2; nnormalize; #H;
 459  ##[ ##62: napply  (bool_destruct … H)
 460  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 461  ##]
 462 nqed.
 463
 464 nlemma neqascii_to_neq63 : ∀a2.eq_ascii ch_z a2 = false → ch_z ≠ a2.
 465  #a2; ncases a2; nnormalize; #H;
 466  ##[ ##63: napply  (bool_destruct … H)
 467  ##| ##*: #H1; napply False_ind; napply (ascii_destruct … H1)
 468  ##]
 469 nqed.
 470
 471 nlemma neqascii_to_neq : ∀c1,c2.eq_ascii c1 c2 = false → c1 ≠ c2.
 472  #c1; ncases c1;
 473  ##[ ##1: napply neqascii_to_neq1 ##| ##2: napply neqascii_to_neq2
 474  ##| ##3: napply neqascii_to_neq3 ##| ##4: napply neqascii_to_neq4
 475  ##| ##5: napply neqascii_to_neq5 ##| ##6: napply neqascii_to_neq6
 476  ##| ##7: napply neqascii_to_neq7 ##| ##8: napply neqascii_to_neq8
 477  ##| ##9: napply neqascii_to_neq9 ##| ##10: napply neqascii_to_neq10
 478  ##| ##11: napply neqascii_to_neq11 ##| ##12: napply neqascii_to_neq12
 479  ##| ##13: napply neqascii_to_neq13 ##| ##14: napply neqascii_to_neq14
 480  ##| ##15: napply neqascii_to_neq15 ##| ##16: napply neqascii_to_neq16
 481  ##| ##17: napply neqascii_to_neq17 ##| ##18: napply neqascii_to_neq18
 482  ##| ##19: napply neqascii_to_neq19 ##| ##20: napply neqascii_to_neq20
 483  ##| ##21: napply neqascii_to_neq21 ##| ##22: napply neqascii_to_neq22
 484  ##| ##23: napply neqascii_to_neq23 ##| ##24: napply neqascii_to_neq24
 485  ##| ##25: napply neqascii_to_neq25 ##| ##26: napply neqascii_to_neq26
 486  ##| ##27: napply neqascii_to_neq27 ##| ##28: napply neqascii_to_neq28
 487  ##| ##29: napply neqascii_to_neq29 ##| ##30: napply neqascii_to_neq30
 488  ##| ##31: napply neqascii_to_neq31 ##| ##32: napply neqascii_to_neq32
 489  ##| ##33: napply neqascii_to_neq33 ##| ##34: napply neqascii_to_neq34
 490  ##| ##35: napply neqascii_to_neq35 ##| ##36: napply neqascii_to_neq36
 491  ##| ##37: napply neqascii_to_neq37 ##| ##38: napply neqascii_to_neq38
 492  ##| ##39: napply neqascii_to_neq39 ##| ##40: napply neqascii_to_neq40
 493  ##| ##41: napply neqascii_to_neq41 ##| ##42: napply neqascii_to_neq42
 494  ##| ##43: napply neqascii_to_neq43 ##| ##44: napply neqascii_to_neq44
 495  ##| ##45: napply neqascii_to_neq45 ##| ##46: napply neqascii_to_neq46
 496  ##| ##47: napply neqascii_to_neq47 ##| ##48: napply neqascii_to_neq48
 497  ##| ##49: napply neqascii_to_neq49 ##| ##50: napply neqascii_to_neq50
 498  ##| ##51: napply neqascii_to_neq51 ##| ##52: napply neqascii_to_neq52
 499  ##| ##53: napply neqascii_to_neq53 ##| ##54: napply neqascii_to_neq54
 500  ##| ##55: napply neqascii_to_neq55 ##| ##56: napply neqascii_to_neq56
 501  ##| ##57: napply neqascii_to_neq57 ##| ##58: napply neqascii_to_neq58
 502  ##| ##59: napply neqascii_to_neq59 ##| ##60: napply neqascii_to_neq60
 503  ##| ##61: napply neqascii_to_neq61 ##| ##62: napply neqascii_to_neq62
 504  ##| ##63: napply neqascii_to_neq63 ##]
 505 nqed.