helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas2.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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "utility/ascii_lemmas1.ma".
  24 include "freescale/bool_lemmas.ma".
  25
  26 (* ************************** *)
  27 (* DEFINIZIONE ASCII MINIMALE *)
  28 (* ************************** *)
  29
  30 nlemma symmetric_eqascii1 : ∀a2.eq_ascii ch_0 a2 = eq_ascii a2 ch_0. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  31 nlemma symmetric_eqascii2 : ∀a2.eq_ascii ch_1 a2 = eq_ascii a2 ch_1. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  32 nlemma symmetric_eqascii3 : ∀a2.eq_ascii ch_2 a2 = eq_ascii a2 ch_2. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  33 nlemma symmetric_eqascii4 : ∀a2.eq_ascii ch_3 a2 = eq_ascii a2 ch_3. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  34 nlemma symmetric_eqascii5 : ∀a2.eq_ascii ch_4 a2 = eq_ascii a2 ch_4. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  35 nlemma symmetric_eqascii6 : ∀a2.eq_ascii ch_5 a2 = eq_ascii a2 ch_5. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  36 nlemma symmetric_eqascii7 : ∀a2.eq_ascii ch_6 a2 = eq_ascii a2 ch_6. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  37 nlemma symmetric_eqascii8 : ∀a2.eq_ascii ch_7 a2 = eq_ascii a2 ch_7. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  38 nlemma symmetric_eqascii9 : ∀a2.eq_ascii ch_8 a2 = eq_ascii a2 ch_8. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  39 nlemma symmetric_eqascii10 : ∀a2.eq_ascii ch_9 a2 = eq_ascii a2 ch_9. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  40 nlemma symmetric_eqascii11 : ∀a2.eq_ascii ch__ a2 = eq_ascii a2 ch__. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  41 nlemma symmetric_eqascii12 : ∀a2.eq_ascii ch_A a2 = eq_ascii a2 ch_A. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  42 nlemma symmetric_eqascii13 : ∀a2.eq_ascii ch_B a2 = eq_ascii a2 ch_B. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  43 nlemma symmetric_eqascii14 : ∀a2.eq_ascii ch_C a2 = eq_ascii a2 ch_C. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  44 nlemma symmetric_eqascii15 : ∀a2.eq_ascii ch_D a2 = eq_ascii a2 ch_D. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  45 nlemma symmetric_eqascii16 : ∀a2.eq_ascii ch_E a2 = eq_ascii a2 ch_E. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  46 nlemma symmetric_eqascii17 : ∀a2.eq_ascii ch_F a2 = eq_ascii a2 ch_F. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  47 nlemma symmetric_eqascii18 : ∀a2.eq_ascii ch_G a2 = eq_ascii a2 ch_G. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  48 nlemma symmetric_eqascii19 : ∀a2.eq_ascii ch_H a2 = eq_ascii a2 ch_H. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  49 nlemma symmetric_eqascii20 : ∀a2.eq_ascii ch_I a2 = eq_ascii a2 ch_I. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  50 nlemma symmetric_eqascii21 : ∀a2.eq_ascii ch_J a2 = eq_ascii a2 ch_J. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  51 nlemma symmetric_eqascii22 : ∀a2.eq_ascii ch_K a2 = eq_ascii a2 ch_K. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  52 nlemma symmetric_eqascii23 : ∀a2.eq_ascii ch_L a2 = eq_ascii a2 ch_L. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  53 nlemma symmetric_eqascii24 : ∀a2.eq_ascii ch_M a2 = eq_ascii a2 ch_M. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  54 nlemma symmetric_eqascii25 : ∀a2.eq_ascii ch_N a2 = eq_ascii a2 ch_N. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  55 nlemma symmetric_eqascii26 : ∀a2.eq_ascii ch_O a2 = eq_ascii a2 ch_O. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  56 nlemma symmetric_eqascii27 : ∀a2.eq_ascii ch_P a2 = eq_ascii a2 ch_P. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  57 nlemma symmetric_eqascii28 : ∀a2.eq_ascii ch_Q a2 = eq_ascii a2 ch_Q. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  58 nlemma symmetric_eqascii29 : ∀a2.eq_ascii ch_R a2 = eq_ascii a2 ch_R. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  59 nlemma symmetric_eqascii30 : ∀a2.eq_ascii ch_S a2 = eq_ascii a2 ch_S. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  60 nlemma symmetric_eqascii31 : ∀a2.eq_ascii ch_T a2 = eq_ascii a2 ch_T. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  61 nlemma symmetric_eqascii32 : ∀a2.eq_ascii ch_U a2 = eq_ascii a2 ch_U. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  62 nlemma symmetric_eqascii33 : ∀a2.eq_ascii ch_V a2 = eq_ascii a2 ch_V. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  63 nlemma symmetric_eqascii34 : ∀a2.eq_ascii ch_W a2 = eq_ascii a2 ch_W. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  64 nlemma symmetric_eqascii35 : ∀a2.eq_ascii ch_X a2 = eq_ascii a2 ch_X. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  65 nlemma symmetric_eqascii36 : ∀a2.eq_ascii ch_Y a2 = eq_ascii a2 ch_Y. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  66 nlemma symmetric_eqascii37 : ∀a2.eq_ascii ch_Z a2 = eq_ascii a2 ch_Z. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  67 nlemma symmetric_eqascii38 : ∀a2.eq_ascii ch_a a2 = eq_ascii a2 ch_a. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  68 nlemma symmetric_eqascii39 : ∀a2.eq_ascii ch_b a2 = eq_ascii a2 ch_b. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  69 nlemma symmetric_eqascii40 : ∀a2.eq_ascii ch_c a2 = eq_ascii a2 ch_c. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  70 nlemma symmetric_eqascii41 : ∀a2.eq_ascii ch_d a2 = eq_ascii a2 ch_d. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  71 nlemma symmetric_eqascii42 : ∀a2.eq_ascii ch_e a2 = eq_ascii a2 ch_e. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  72 nlemma symmetric_eqascii43 : ∀a2.eq_ascii ch_f a2 = eq_ascii a2 ch_f. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  73 nlemma symmetric_eqascii44 : ∀a2.eq_ascii ch_g a2 = eq_ascii a2 ch_g. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  74 nlemma symmetric_eqascii45 : ∀a2.eq_ascii ch_h a2 = eq_ascii a2 ch_h. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  75 nlemma symmetric_eqascii46 : ∀a2.eq_ascii ch_i a2 = eq_ascii a2 ch_i. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  76 nlemma symmetric_eqascii47 : ∀a2.eq_ascii ch_j a2 = eq_ascii a2 ch_j. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  77 nlemma symmetric_eqascii48 : ∀a2.eq_ascii ch_k a2 = eq_ascii a2 ch_k. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  78 nlemma symmetric_eqascii49 : ∀a2.eq_ascii ch_l a2 = eq_ascii a2 ch_l. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  79 nlemma symmetric_eqascii50 : ∀a2.eq_ascii ch_m a2 = eq_ascii a2 ch_m. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  80 nlemma symmetric_eqascii51 : ∀a2.eq_ascii ch_n a2 = eq_ascii a2 ch_n. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  81 nlemma symmetric_eqascii52 : ∀a2.eq_ascii ch_o a2 = eq_ascii a2 ch_o. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  82 nlemma symmetric_eqascii53 : ∀a2.eq_ascii ch_p a2 = eq_ascii a2 ch_p. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  83 nlemma symmetric_eqascii54 : ∀a2.eq_ascii ch_q a2 = eq_ascii a2 ch_q. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  84 nlemma symmetric_eqascii55 : ∀a2.eq_ascii ch_r a2 = eq_ascii a2 ch_r. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  85 nlemma symmetric_eqascii56 : ∀a2.eq_ascii ch_s a2 = eq_ascii a2 ch_s. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  86 nlemma symmetric_eqascii57 : ∀a2.eq_ascii ch_t a2 = eq_ascii a2 ch_t. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  87 nlemma symmetric_eqascii58 : ∀a2.eq_ascii ch_u a2 = eq_ascii a2 ch_u. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  88 nlemma symmetric_eqascii59 : ∀a2.eq_ascii ch_v a2 = eq_ascii a2 ch_v. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  89 nlemma symmetric_eqascii60 : ∀a2.eq_ascii ch_w a2 = eq_ascii a2 ch_w. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  90 nlemma symmetric_eqascii61 : ∀a2.eq_ascii ch_x a2 = eq_ascii a2 ch_x. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  91 nlemma symmetric_eqascii62 : ∀a2.eq_ascii ch_y a2 = eq_ascii a2 ch_y. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  92 nlemma symmetric_eqascii63 : ∀a2.eq_ascii ch_z a2 = eq_ascii a2 ch_z. #a2; ncases a2; nnormalize; napply (refl_eq ??).nqed.
  93
  94 nlemma symmetric_eqascii : symmetricT ascii bool eq_ascii.
  95  #a1; ncases a1;
  96  ##[ ##1: napply symmetric_eqascii1 ##| ##2: napply symmetric_eqascii2
  97  ##| ##3: napply symmetric_eqascii3 ##| ##4: napply symmetric_eqascii4
  98  ##| ##5: napply symmetric_eqascii5 ##| ##6: napply symmetric_eqascii6
  99  ##| ##7: napply symmetric_eqascii7 ##| ##8: napply symmetric_eqascii8
 100  ##| ##9: napply symmetric_eqascii9 ##| ##10: napply symmetric_eqascii10
 101  ##| ##11: napply symmetric_eqascii11 ##| ##12: napply symmetric_eqascii12
 102  ##| ##13: napply symmetric_eqascii13 ##| ##14: napply symmetric_eqascii14
 103  ##| ##15: napply symmetric_eqascii15 ##| ##16: napply symmetric_eqascii16
 104  ##| ##17: napply symmetric_eqascii17 ##| ##18: napply symmetric_eqascii18
 105  ##| ##19: napply symmetric_eqascii19 ##| ##20: napply symmetric_eqascii20
 106  ##| ##21: napply symmetric_eqascii21 ##| ##22: napply symmetric_eqascii22
 107  ##| ##23: napply symmetric_eqascii23 ##| ##24: napply symmetric_eqascii24
 108  ##| ##25: napply symmetric_eqascii25 ##| ##26: napply symmetric_eqascii26
 109  ##| ##27: napply symmetric_eqascii27 ##| ##28: napply symmetric_eqascii28
 110  ##| ##29: napply symmetric_eqascii29 ##| ##30: napply symmetric_eqascii30
 111  ##| ##31: napply symmetric_eqascii31 ##| ##32: napply symmetric_eqascii32
 112  ##| ##33: napply symmetric_eqascii33 ##| ##34: napply symmetric_eqascii34
 113  ##| ##35: napply symmetric_eqascii35 ##| ##36: napply symmetric_eqascii36
 114  ##| ##37: napply symmetric_eqascii37 ##| ##38: napply symmetric_eqascii38
 115  ##| ##39: napply symmetric_eqascii39 ##| ##40: napply symmetric_eqascii40
 116  ##| ##41: napply symmetric_eqascii41 ##| ##42: napply symmetric_eqascii42
 117  ##| ##43: napply symmetric_eqascii43 ##| ##44: napply symmetric_eqascii44
 118  ##| ##45: napply symmetric_eqascii45 ##| ##46: napply symmetric_eqascii46
 119  ##| ##47: napply symmetric_eqascii47 ##| ##48: napply symmetric_eqascii48
 120  ##| ##49: napply symmetric_eqascii49 ##| ##50: napply symmetric_eqascii50
 121  ##| ##51: napply symmetric_eqascii51 ##| ##52: napply symmetric_eqascii52
 122  ##| ##53: napply symmetric_eqascii53 ##| ##54: napply symmetric_eqascii54
 123  ##| ##55: napply symmetric_eqascii55 ##| ##56: napply symmetric_eqascii56
 124  ##| ##57: napply symmetric_eqascii57 ##| ##58: napply symmetric_eqascii58
 125  ##| ##59: napply symmetric_eqascii59 ##| ##60: napply symmetric_eqascii60
 126  ##| ##61: napply symmetric_eqascii61 ##| ##62: napply symmetric_eqascii62
 127  ##| ##63: napply symmetric_eqascii63 ##]
 128 nqed.
 129
 130 nlemma eqascii_to_eq1 : ∀a2.eq_ascii ch_0 a2 = true → ch_0 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 131 nlemma eqascii_to_eq2 : ∀a2.eq_ascii ch_1 a2 = true → ch_1 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 132 nlemma eqascii_to_eq3 : ∀a2.eq_ascii ch_2 a2 = true → ch_2 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 133 nlemma eqascii_to_eq4 : ∀a2.eq_ascii ch_3 a2 = true → ch_3 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 134 nlemma eqascii_to_eq5 : ∀a2.eq_ascii ch_4 a2 = true → ch_4 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 135 nlemma eqascii_to_eq6 : ∀a2.eq_ascii ch_5 a2 = true → ch_5 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 136 nlemma eqascii_to_eq7 : ∀a2.eq_ascii ch_6 a2 = true → ch_6 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 137 nlemma eqascii_to_eq8 : ∀a2.eq_ascii ch_7 a2 = true → ch_7 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 138 nlemma eqascii_to_eq9 : ∀a2.eq_ascii ch_8 a2 = true → ch_8 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 139 nlemma eqascii_to_eq10 : ∀a2.eq_ascii ch_9 a2 = true → ch_9 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 140 nlemma eqascii_to_eq11 : ∀a2.eq_ascii ch__ a2 = true → ch__ = a2. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 141 nlemma eqascii_to_eq12 : ∀a2.eq_ascii ch_A a2 = true → ch_A = a2. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 142 nlemma eqascii_to_eq13 : ∀a2.eq_ascii ch_B a2 = true → ch_B = a2. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 143 nlemma eqascii_to_eq14 : ∀a2.eq_ascii ch_C a2 = true → ch_C = a2. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 144 nlemma eqascii_to_eq15 : ∀a2.eq_ascii ch_D a2 = true → ch_D = a2. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 145 nlemma eqascii_to_eq16 : ∀a2.eq_ascii ch_E a2 = true → ch_E = a2. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 146 nlemma eqascii_to_eq17 : ∀a2.eq_ascii ch_F a2 = true → ch_F = a2. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 147 nlemma eqascii_to_eq18 : ∀a2.eq_ascii ch_G a2 = true → ch_G = a2. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 148 nlemma eqascii_to_eq19 : ∀a2.eq_ascii ch_H a2 = true → ch_H = a2. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 149 nlemma eqascii_to_eq20 : ∀a2.eq_ascii ch_I a2 = true → ch_I = a2. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 150 nlemma eqascii_to_eq21 : ∀a2.eq_ascii ch_J a2 = true → ch_J = a2. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 151 nlemma eqascii_to_eq22 : ∀a2.eq_ascii ch_K a2 = true → ch_K = a2. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 152 nlemma eqascii_to_eq23 : ∀a2.eq_ascii ch_L a2 = true → ch_L = a2. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 153 nlemma eqascii_to_eq24 : ∀a2.eq_ascii ch_M a2 = true → ch_M = a2. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 154 nlemma eqascii_to_eq25 : ∀a2.eq_ascii ch_N a2 = true → ch_N = a2. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 155 nlemma eqascii_to_eq26 : ∀a2.eq_ascii ch_O a2 = true → ch_O = a2. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 156 nlemma eqascii_to_eq27 : ∀a2.eq_ascii ch_P a2 = true → ch_P = a2. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 157 nlemma eqascii_to_eq28 : ∀a2.eq_ascii ch_Q a2 = true → ch_Q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 158 nlemma eqascii_to_eq29 : ∀a2.eq_ascii ch_R a2 = true → ch_R = a2. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 159 nlemma eqascii_to_eq30 : ∀a2.eq_ascii ch_S a2 = true → ch_S = a2. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 160 nlemma eqascii_to_eq31 : ∀a2.eq_ascii ch_T a2 = true → ch_T = a2. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 161 nlemma eqascii_to_eq32 : ∀a2.eq_ascii ch_U a2 = true → ch_U = a2. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 162 nlemma eqascii_to_eq33 : ∀a2.eq_ascii ch_V a2 = true → ch_V = a2. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 163 nlemma eqascii_to_eq34 : ∀a2.eq_ascii ch_W a2 = true → ch_W = a2. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 164 nlemma eqascii_to_eq35 : ∀a2.eq_ascii ch_X a2 = true → ch_X = a2. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 165 nlemma eqascii_to_eq36 : ∀a2.eq_ascii ch_Y a2 = true → ch_Y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 166 nlemma eqascii_to_eq37 : ∀a2.eq_ascii ch_Z a2 = true → ch_Z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 167 nlemma eqascii_to_eq38 : ∀a2.eq_ascii ch_a a2 = true → ch_a = a2. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 168 nlemma eqascii_to_eq39 : ∀a2.eq_ascii ch_b a2 = true → ch_b = a2. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 169 nlemma eqascii_to_eq40 : ∀a2.eq_ascii ch_c a2 = true → ch_c = a2. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 170 nlemma eqascii_to_eq41 : ∀a2.eq_ascii ch_d a2 = true → ch_d = a2. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 171 nlemma eqascii_to_eq42 : ∀a2.eq_ascii ch_e a2 = true → ch_e = a2. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 172 nlemma eqascii_to_eq43 : ∀a2.eq_ascii ch_f a2 = true → ch_f = a2. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 173 nlemma eqascii_to_eq44 : ∀a2.eq_ascii ch_g a2 = true → ch_g = a2. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 174 nlemma eqascii_to_eq45 : ∀a2.eq_ascii ch_h a2 = true → ch_h = a2. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 175 nlemma eqascii_to_eq46 : ∀a2.eq_ascii ch_i a2 = true → ch_i = a2. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 176 nlemma eqascii_to_eq47 : ∀a2.eq_ascii ch_j a2 = true → ch_j = a2. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 177 nlemma eqascii_to_eq48 : ∀a2.eq_ascii ch_k a2 = true → ch_k = a2. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 178 nlemma eqascii_to_eq49 : ∀a2.eq_ascii ch_l a2 = true → ch_l = a2. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 179 nlemma eqascii_to_eq50 : ∀a2.eq_ascii ch_m a2 = true → ch_m = a2. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 180 nlemma eqascii_to_eq51 : ∀a2.eq_ascii ch_n a2 = true → ch_n = a2. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 181 nlemma eqascii_to_eq52 : ∀a2.eq_ascii ch_o a2 = true → ch_o = a2. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 182 nlemma eqascii_to_eq53 : ∀a2.eq_ascii ch_p a2 = true → ch_p = a2. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 183 nlemma eqascii_to_eq54 : ∀a2.eq_ascii ch_q a2 = true → ch_q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 184 nlemma eqascii_to_eq55 : ∀a2.eq_ascii ch_r a2 = true → ch_r = a2. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 185 nlemma eqascii_to_eq56 : ∀a2.eq_ascii ch_s a2 = true → ch_s = a2. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 186 nlemma eqascii_to_eq57 : ∀a2.eq_ascii ch_t a2 = true → ch_t = a2. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 187 nlemma eqascii_to_eq58 : ∀a2.eq_ascii ch_u a2 = true → ch_u = a2. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 188 nlemma eqascii_to_eq59 : ∀a2.eq_ascii ch_v a2 = true → ch_v = a2. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 189 nlemma eqascii_to_eq60 : ∀a2.eq_ascii ch_w a2 = true → ch_w = a2. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 190 nlemma eqascii_to_eq61 : ∀a2.eq_ascii ch_x a2 = true → ch_x = a2. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 191 nlemma eqascii_to_eq62 : ∀a2.eq_ascii ch_y a2 = true → ch_y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 192 nlemma eqascii_to_eq63 : ∀a2.eq_ascii ch_z a2 = true → ch_z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply (refl_eq ??) | ##*: napply (bool_destruct ??? H) ##] nqed.
 193
 194 nlemma eqascii_to_eq : ∀c1,c2.eq_ascii c1 c2 = true → c1 = c2.
 195  #c1; ncases c1;
 196  ##[ ##1: napply eqascii_to_eq1 ##| ##2: napply eqascii_to_eq2
 197  ##| ##3: napply eqascii_to_eq3 ##| ##4: napply eqascii_to_eq4
 198  ##| ##5: napply eqascii_to_eq5 ##| ##6: napply eqascii_to_eq6
 199  ##| ##7: napply eqascii_to_eq7 ##| ##8: napply eqascii_to_eq8
 200  ##| ##9: napply eqascii_to_eq9 ##| ##10: napply eqascii_to_eq10
 201  ##| ##11: napply eqascii_to_eq11 ##| ##12: napply eqascii_to_eq12
 202  ##| ##13: napply eqascii_to_eq13 ##| ##14: napply eqascii_to_eq14
 203  ##| ##15: napply eqascii_to_eq15 ##| ##16: napply eqascii_to_eq16
 204  ##| ##17: napply eqascii_to_eq17 ##| ##18: napply eqascii_to_eq18
 205  ##| ##19: napply eqascii_to_eq19 ##| ##20: napply eqascii_to_eq20
 206  ##| ##21: napply eqascii_to_eq21 ##| ##22: napply eqascii_to_eq22
 207  ##| ##23: napply eqascii_to_eq23 ##| ##24: napply eqascii_to_eq24
 208  ##| ##25: napply eqascii_to_eq25 ##| ##26: napply eqascii_to_eq26
 209  ##| ##27: napply eqascii_to_eq27 ##| ##28: napply eqascii_to_eq28
 210  ##| ##29: napply eqascii_to_eq29 ##| ##30: napply eqascii_to_eq30
 211  ##| ##31: napply eqascii_to_eq31 ##| ##32: napply eqascii_to_eq32
 212  ##| ##33: napply eqascii_to_eq33 ##| ##34: napply eqascii_to_eq34
 213  ##| ##35: napply eqascii_to_eq35 ##| ##36: napply eqascii_to_eq36
 214  ##| ##37: napply eqascii_to_eq37 ##| ##38: napply eqascii_to_eq38
 215  ##| ##39: napply eqascii_to_eq39 ##| ##40: napply eqascii_to_eq40
 216  ##| ##41: napply eqascii_to_eq41 ##| ##42: napply eqascii_to_eq42
 217  ##| ##43: napply eqascii_to_eq43 ##| ##44: napply eqascii_to_eq44
 218  ##| ##45: napply eqascii_to_eq45 ##| ##46: napply eqascii_to_eq46
 219  ##| ##47: napply eqascii_to_eq47 ##| ##48: napply eqascii_to_eq48
 220  ##| ##49: napply eqascii_to_eq49 ##| ##50: napply eqascii_to_eq50
 221  ##| ##51: napply eqascii_to_eq51 ##| ##52: napply eqascii_to_eq52
 222  ##| ##53: napply eqascii_to_eq53 ##| ##54: napply eqascii_to_eq54
 223  ##| ##55: napply eqascii_to_eq55 ##| ##56: napply eqascii_to_eq56
 224  ##| ##57: napply eqascii_to_eq57 ##| ##58: napply eqascii_to_eq58
 225  ##| ##59: napply eqascii_to_eq59 ##| ##60: napply eqascii_to_eq60
 226  ##| ##61: napply eqascii_to_eq61 ##| ##62: napply eqascii_to_eq62
 227  ##| ##63: napply eqascii_to_eq63 ##]
 228 nqed.
 229
 230 nlemma eq_to_eqascii1 : ∀a2.ch_0 = a2 → eq_ascii ch_0 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 231 nlemma eq_to_eqascii2 : ∀a2.ch_1 = a2 → eq_ascii ch_1 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 232 nlemma eq_to_eqascii3 : ∀a2.ch_2 = a2 → eq_ascii ch_2 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 233 nlemma eq_to_eqascii4 : ∀a2.ch_3 = a2 → eq_ascii ch_3 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 234 nlemma eq_to_eqascii5 : ∀a2.ch_4 = a2 → eq_ascii ch_4 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 235 nlemma eq_to_eqascii6 : ∀a2.ch_5 = a2 → eq_ascii ch_5 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 236 nlemma eq_to_eqascii7 : ∀a2.ch_6 = a2 → eq_ascii ch_6 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 237 nlemma eq_to_eqascii8 : ∀a2.ch_7 = a2 → eq_ascii ch_7 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 238 nlemma eq_to_eqascii9 : ∀a2.ch_8 = a2 → eq_ascii ch_8 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 239 nlemma eq_to_eqascii10 : ∀a2.ch_9 = a2 → eq_ascii ch_9 a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 240 nlemma eq_to_eqascii11 : ∀a2.ch__ = a2 → eq_ascii ch__ a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 241 nlemma eq_to_eqascii12 : ∀a2.ch_A = a2 → eq_ascii ch_A a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 242 nlemma eq_to_eqascii13 : ∀a2.ch_B = a2 → eq_ascii ch_B a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 243 nlemma eq_to_eqascii14 : ∀a2.ch_C = a2 → eq_ascii ch_C a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 244 nlemma eq_to_eqascii15 : ∀a2.ch_D = a2 → eq_ascii ch_D a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 245 nlemma eq_to_eqascii16 : ∀a2.ch_E = a2 → eq_ascii ch_E a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 246 nlemma eq_to_eqascii17 : ∀a2.ch_F = a2 → eq_ascii ch_F a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 247 nlemma eq_to_eqascii18 : ∀a2.ch_G = a2 → eq_ascii ch_G a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 248 nlemma eq_to_eqascii19 : ∀a2.ch_H = a2 → eq_ascii ch_H a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 249 nlemma eq_to_eqascii20 : ∀a2.ch_I = a2 → eq_ascii ch_I a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 250 nlemma eq_to_eqascii21 : ∀a2.ch_J = a2 → eq_ascii ch_J a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 251 nlemma eq_to_eqascii22 : ∀a2.ch_K = a2 → eq_ascii ch_K a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 252 nlemma eq_to_eqascii23 : ∀a2.ch_L = a2 → eq_ascii ch_L a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 253 nlemma eq_to_eqascii24 : ∀a2.ch_M = a2 → eq_ascii ch_M a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 254 nlemma eq_to_eqascii25 : ∀a2.ch_N = a2 → eq_ascii ch_N a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 255 nlemma eq_to_eqascii26 : ∀a2.ch_O = a2 → eq_ascii ch_O a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 256 nlemma eq_to_eqascii27 : ∀a2.ch_P = a2 → eq_ascii ch_P a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 257 nlemma eq_to_eqascii28 : ∀a2.ch_Q = a2 → eq_ascii ch_Q a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 258 nlemma eq_to_eqascii29 : ∀a2.ch_R = a2 → eq_ascii ch_R a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 259 nlemma eq_to_eqascii30 : ∀a2.ch_S = a2 → eq_ascii ch_S a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 260 nlemma eq_to_eqascii31 : ∀a2.ch_T = a2 → eq_ascii ch_T a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 261 nlemma eq_to_eqascii32 : ∀a2.ch_U = a2 → eq_ascii ch_U a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 262 nlemma eq_to_eqascii33 : ∀a2.ch_V = a2 → eq_ascii ch_V a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 263 nlemma eq_to_eqascii34 : ∀a2.ch_W = a2 → eq_ascii ch_W a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 264 nlemma eq_to_eqascii35 : ∀a2.ch_X = a2 → eq_ascii ch_X a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 265 nlemma eq_to_eqascii36 : ∀a2.ch_Y = a2 → eq_ascii ch_Y a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 266 nlemma eq_to_eqascii37 : ∀a2.ch_Z = a2 → eq_ascii ch_Z a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 267 nlemma eq_to_eqascii38 : ∀a2.ch_a = a2 → eq_ascii ch_a a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 268 nlemma eq_to_eqascii39 : ∀a2.ch_b = a2 → eq_ascii ch_b a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 269 nlemma eq_to_eqascii40 : ∀a2.ch_c = a2 → eq_ascii ch_c a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 270 nlemma eq_to_eqascii41 : ∀a2.ch_d = a2 → eq_ascii ch_d a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 271 nlemma eq_to_eqascii42 : ∀a2.ch_e = a2 → eq_ascii ch_e a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 272 nlemma eq_to_eqascii43 : ∀a2.ch_f = a2 → eq_ascii ch_f a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 273 nlemma eq_to_eqascii44 : ∀a2.ch_g = a2 → eq_ascii ch_g a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 274 nlemma eq_to_eqascii45 : ∀a2.ch_h = a2 → eq_ascii ch_h a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 275 nlemma eq_to_eqascii46 : ∀a2.ch_i = a2 → eq_ascii ch_i a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 276 nlemma eq_to_eqascii47 : ∀a2.ch_j = a2 → eq_ascii ch_j a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 277 nlemma eq_to_eqascii48 : ∀a2.ch_k = a2 → eq_ascii ch_k a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 278 nlemma eq_to_eqascii49 : ∀a2.ch_l = a2 → eq_ascii ch_l a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 279 nlemma eq_to_eqascii50 : ∀a2.ch_m = a2 → eq_ascii ch_m a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 280 nlemma eq_to_eqascii51 : ∀a2.ch_n = a2 → eq_ascii ch_n a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 281 nlemma eq_to_eqascii52 : ∀a2.ch_o = a2 → eq_ascii ch_o a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 282 nlemma eq_to_eqascii53 : ∀a2.ch_p = a2 → eq_ascii ch_p a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 283 nlemma eq_to_eqascii54 : ∀a2.ch_q = a2 → eq_ascii ch_q a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 284 nlemma eq_to_eqascii55 : ∀a2.ch_r = a2 → eq_ascii ch_r a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 285 nlemma eq_to_eqascii56 : ∀a2.ch_s = a2 → eq_ascii ch_s a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 286 nlemma eq_to_eqascii57 : ∀a2.ch_t = a2 → eq_ascii ch_t a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 287 nlemma eq_to_eqascii58 : ∀a2.ch_u = a2 → eq_ascii ch_u a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 288 nlemma eq_to_eqascii59 : ∀a2.ch_v = a2 → eq_ascii ch_v a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 289 nlemma eq_to_eqascii60 : ∀a2.ch_w = a2 → eq_ascii ch_w a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 290 nlemma eq_to_eqascii61 : ∀a2.ch_x = a2 → eq_ascii ch_x a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 291 nlemma eq_to_eqascii62 : ∀a2.ch_y = a2 → eq_ascii ch_y a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 292 nlemma eq_to_eqascii63 : ∀a2.ch_z = a2 → eq_ascii ch_z a2 = true. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply (refl_eq ??) | ##*: napply (ascii_destruct ??? H) ##] nqed.
 293
 294 nlemma eq_to_eqascii : ∀c1,c2.c1 = c2 → eq_ascii c1 c2 = true.
 295  #c1; ncases c1;
 296  ##[ ##1: napply eq_to_eqascii1 ##| ##2: napply eq_to_eqascii2
 297  ##| ##3: napply eq_to_eqascii3 ##| ##4: napply eq_to_eqascii4
 298  ##| ##5: napply eq_to_eqascii5 ##| ##6: napply eq_to_eqascii6
 299  ##| ##7: napply eq_to_eqascii7 ##| ##8: napply eq_to_eqascii8
 300  ##| ##9: napply eq_to_eqascii9 ##| ##10: napply eq_to_eqascii10
 301  ##| ##11: napply eq_to_eqascii11 ##| ##12: napply eq_to_eqascii12
 302  ##| ##13: napply eq_to_eqascii13 ##| ##14: napply eq_to_eqascii14
 303  ##| ##15: napply eq_to_eqascii15 ##| ##16: napply eq_to_eqascii16
 304  ##| ##17: napply eq_to_eqascii17 ##| ##18: napply eq_to_eqascii18
 305  ##| ##19: napply eq_to_eqascii19 ##| ##20: napply eq_to_eqascii20
 306  ##| ##21: napply eq_to_eqascii21 ##| ##22: napply eq_to_eqascii22
 307  ##| ##23: napply eq_to_eqascii23 ##| ##24: napply eq_to_eqascii24
 308  ##| ##25: napply eq_to_eqascii25 ##| ##26: napply eq_to_eqascii26
 309  ##| ##27: napply eq_to_eqascii27 ##| ##28: napply eq_to_eqascii28
 310  ##| ##29: napply eq_to_eqascii29 ##| ##30: napply eq_to_eqascii30
 311  ##| ##31: napply eq_to_eqascii31 ##| ##32: napply eq_to_eqascii32
 312  ##| ##33: napply eq_to_eqascii33 ##| ##34: napply eq_to_eqascii34
 313  ##| ##35: napply eq_to_eqascii35 ##| ##36: napply eq_to_eqascii36
 314  ##| ##37: napply eq_to_eqascii37 ##| ##38: napply eq_to_eqascii38
 315  ##| ##39: napply eq_to_eqascii39 ##| ##40: napply eq_to_eqascii40
 316  ##| ##41: napply eq_to_eqascii41 ##| ##42: napply eq_to_eqascii42
 317  ##| ##43: napply eq_to_eqascii43 ##| ##44: napply eq_to_eqascii44
 318  ##| ##45: napply eq_to_eqascii45 ##| ##46: napply eq_to_eqascii46
 319  ##| ##47: napply eq_to_eqascii47 ##| ##48: napply eq_to_eqascii48
 320  ##| ##49: napply eq_to_eqascii49 ##| ##50: napply eq_to_eqascii50
 321  ##| ##51: napply eq_to_eqascii51 ##| ##52: napply eq_to_eqascii52
 322  ##| ##53: napply eq_to_eqascii53 ##| ##54: napply eq_to_eqascii54
 323  ##| ##55: napply eq_to_eqascii55 ##| ##56: napply eq_to_eqascii56
 324  ##| ##57: napply eq_to_eqascii57 ##| ##58: napply eq_to_eqascii58
 325  ##| ##59: napply eq_to_eqascii59 ##| ##60: napply eq_to_eqascii60
 326  ##| ##61: napply eq_to_eqascii61 ##| ##62: napply eq_to_eqascii62
 327  ##| ##63: napply eq_to_eqascii63 ##]
 328 nqed.