helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.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.ma".
  24 include "freescale/theory.ma".
  25
  26 (* ************************** *)
  27 (* DEFINIZIONE ASCII MINIMALE *)
  28 (* ************************** *)
  29
  30 ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ].
  31  #c2; #P; ncases c2; nnormalize;
  32  ##[ ##1: #H; napply (λx:P.x)
  33  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  34  ##]
  35 nqed.
  36
  37 ndefinition ascii_destruct2 : Πc2.ΠP:Prop.ch_1 = c2 → match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ].
  38  #c2; #P; ncases c2; nnormalize;
  39  ##[ ##2: #H; napply (λx:P.x)
  40  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  41  ##]
  42 nqed.
  43
  44 ndefinition ascii_destruct3 : Πc2.ΠP:Prop.ch_2 = c2 → match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ].
  45  #c2; #P; ncases c2; nnormalize;
  46  ##[ ##3: #H; napply (λx:P.x)
  47  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  48  ##]
  49 nqed.
  50
  51 ndefinition ascii_destruct4 : Πc2.ΠP:Prop.ch_3 = c2 → match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ].
  52  #c2; #P; ncases c2; nnormalize;
  53  ##[ ##4: #H; napply (λx:P.x)
  54  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  55  ##]
  56 nqed.
  57
  58 ndefinition ascii_destruct5 : Πc2.ΠP:Prop.ch_4 = c2 → match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ].
  59  #c2; #P; ncases c2; nnormalize;
  60  ##[ ##5: #H; napply (λx:P.x)
  61  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  62  ##]
  63 nqed.
  64
  65 ndefinition ascii_destruct6 : Πc2.ΠP:Prop.ch_5 = c2 → match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ].
  66  #c2; #P; ncases c2; nnormalize;
  67  ##[ ##6: #H; napply (λx:P.x)
  68  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  69  ##]
  70 nqed.
  71
  72 ndefinition ascii_destruct7 : Πc2.ΠP:Prop.ch_6 = c2 → match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ].
  73  #c2; #P; ncases c2; nnormalize;
  74  ##[ ##7: #H; napply (λx:P.x)
  75  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  76  ##]
  77 nqed.
  78
  79 ndefinition ascii_destruct8 : Πc2.ΠP:Prop.ch_7 = c2 → match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ].
  80  #c2; #P; ncases c2; nnormalize;
  81  ##[ ##8: #H; napply (λx:P.x)
  82  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  83  ##]
  84 nqed.
  85
  86 ndefinition ascii_destruct9 : Πc2.ΠP:Prop.ch_8 = c2 → match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ].
  87  #c2; #P; ncases c2; nnormalize;
  88  ##[ ##9: #H; napply (λx:P.x)
  89  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  90  ##]
  91 nqed.
  92
  93 ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ].
  94  #c2; #P; ncases c2; nnormalize;
  95  ##[ ##10: #H; napply (λx:P.x)
  96  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  97  ##]
  98 nqed.
  99
 100 ndefinition ascii_destruct11 : Πc2.ΠP:Prop.ch__ = c2 → match c2 with [ ch__ ⇒ P → P | _ ⇒ P ].
 101  #c2; #P; ncases c2; nnormalize;
 102  ##[ ##11: #H; napply (λx:P.x)
 103  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 104  ##]
 105 nqed.
 106
 107 ndefinition ascii_destruct12 : Πc2.ΠP:Prop.ch_A = c2 → match c2 with [ ch_A ⇒ P → P | _ ⇒ P ].
 108  #c2; #P; ncases c2; nnormalize;
 109  ##[ ##12: #H; napply (λx:P.x)
 110  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 111  ##]
 112 nqed.
 113
 114 ndefinition ascii_destruct13 : Πc2.ΠP:Prop.ch_B = c2 → match c2 with [ ch_B ⇒ P → P | _ ⇒ P ].
 115  #c2; #P; ncases c2; nnormalize;
 116  ##[ ##13: #H; napply (λx:P.x)
 117  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 118  ##]
 119 nqed.
 120
 121 ndefinition ascii_destruct14 : Πc2.ΠP:Prop.ch_C = c2 → match c2 with [ ch_C ⇒ P → P | _ ⇒ P ].
 122  #c2; #P; ncases c2; nnormalize;
 123  ##[ ##14: #H; napply (λx:P.x)
 124  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 125  ##]
 126 nqed.
 127
 128 ndefinition ascii_destruct15 : Πc2.ΠP:Prop.ch_D = c2 → match c2 with [ ch_D ⇒ P → P | _ ⇒ P ].
 129  #c2; #P; ncases c2; nnormalize;
 130  ##[ ##15: #H; napply (λx:P.x)
 131  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 132  ##]
 133 nqed.
 134
 135 ndefinition ascii_destruct16 : Πc2.ΠP:Prop.ch_E = c2 → match c2 with [ ch_E ⇒ P → P | _ ⇒ P ].
 136  #c2; #P; ncases c2; nnormalize;
 137  ##[ ##16: #H; napply (λx:P.x)
 138  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 139  ##]
 140 nqed.
 141
 142 ndefinition ascii_destruct17 : Πc2.ΠP:Prop.ch_F = c2 → match c2 with [ ch_F ⇒ P → P | _ ⇒ P ].
 143  #c2; #P; ncases c2; nnormalize;
 144  ##[ ##17: #H; napply (λx:P.x)
 145  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 146  ##]
 147 nqed.
 148
 149 ndefinition ascii_destruct18 : Πc2.ΠP:Prop.ch_G = c2 → match c2 with [ ch_G ⇒ P → P | _ ⇒ P ].
 150  #c2; #P; ncases c2; nnormalize;
 151  ##[ ##18: #H; napply (λx:P.x)
 152  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 153  ##]
 154 nqed.
 155
 156 ndefinition ascii_destruct19 : Πc2.ΠP:Prop.ch_H = c2 → match c2 with [ ch_H ⇒ P → P | _ ⇒ P ].
 157  #c2; #P; ncases c2; nnormalize;
 158  ##[ ##19: #H; napply (λx:P.x)
 159  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 160  ##]
 161 nqed.
 162
 163 ndefinition ascii_destruct20 : Πc2.ΠP:Prop.ch_I = c2 → match c2 with [ ch_I ⇒ P → P | _ ⇒ P ].
 164  #c2; #P; ncases c2; nnormalize;
 165  ##[ ##20: #H; napply (λx:P.x)
 166  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 167  ##]
 168 nqed.
 169
 170 ndefinition ascii_destruct21 : Πc2.ΠP:Prop.ch_J = c2 → match c2 with [ ch_J ⇒ P → P | _ ⇒ P ].
 171  #c2; #P; ncases c2; nnormalize;
 172  ##[ ##21: #H; napply (λx:P.x)
 173  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 174  ##]
 175 nqed.
 176
 177 ndefinition ascii_destruct22 : Πc2.ΠP:Prop.ch_K = c2 → match c2 with [ ch_K ⇒ P → P | _ ⇒ P ].
 178  #c2; #P; ncases c2; nnormalize;
 179  ##[ ##22: #H; napply (λx:P.x)
 180  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 181  ##]
 182 nqed.
 183
 184 ndefinition ascii_destruct23 : Πc2.ΠP:Prop.ch_L = c2 → match c2 with [ ch_L ⇒ P → P | _ ⇒ P ].
 185  #c2; #P; ncases c2; nnormalize;
 186  ##[ ##23: #H; napply (λx:P.x)
 187  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 188  ##]
 189 nqed.
 190
 191 ndefinition ascii_destruct24 : Πc2.ΠP:Prop.ch_M = c2 → match c2 with [ ch_M ⇒ P → P | _ ⇒ P ].
 192  #c2; #P; ncases c2; nnormalize;
 193  ##[ ##24: #H; napply (λx:P.x)
 194  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 195  ##]
 196 nqed.
 197
 198 ndefinition ascii_destruct25 : Πc2.ΠP:Prop.ch_N = c2 → match c2 with [ ch_N ⇒ P → P | _ ⇒ P ].
 199  #c2; #P; ncases c2; nnormalize;
 200  ##[ ##25: #H; napply (λx:P.x)
 201  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 202  ##]
 203 nqed.
 204
 205 ndefinition ascii_destruct26 : Πc2.ΠP:Prop.ch_O = c2 → match c2 with [ ch_O ⇒ P → P | _ ⇒ P ].
 206  #c2; #P; ncases c2; nnormalize;
 207  ##[ ##26: #H; napply (λx:P.x)
 208  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 209  ##]
 210 nqed.
 211
 212 ndefinition ascii_destruct27 : Πc2.ΠP:Prop.ch_P = c2 → match c2 with [ ch_P ⇒ P → P | _ ⇒ P ].
 213  #c2; #P; ncases c2; nnormalize;
 214  ##[ ##27: #H; napply (λx:P.x)
 215  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 216  ##]
 217 nqed.
 218
 219 ndefinition ascii_destruct28 : Πc2.ΠP:Prop.ch_Q = c2 → match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ].
 220  #c2; #P; ncases c2; nnormalize;
 221  ##[ ##28: #H; napply (λx:P.x)
 222  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 223  ##]
 224 nqed.
 225
 226 ndefinition ascii_destruct29 : Πc2.ΠP:Prop.ch_R = c2 → match c2 with [ ch_R ⇒ P → P | _ ⇒ P ].
 227  #c2; #P; ncases c2; nnormalize;
 228  ##[ ##29: #H; napply (λx:P.x)
 229  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 230  ##]
 231 nqed.
 232
 233 ndefinition ascii_destruct30 : Πc2.ΠP:Prop.ch_S = c2 → match c2 with [ ch_S ⇒ P → P | _ ⇒ P ].
 234  #c2; #P; ncases c2; nnormalize;
 235  ##[ ##30: #H; napply (λx:P.x)
 236  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 237  ##]
 238 nqed.
 239
 240 ndefinition ascii_destruct31 : Πc2.ΠP:Prop.ch_T = c2 → match c2 with [ ch_T ⇒ P → P | _ ⇒ P ].
 241  #c2; #P; ncases c2; nnormalize;
 242  ##[ ##31: #H; napply (λx:P.x)
 243  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 244  ##]
 245 nqed.
 246
 247 ndefinition ascii_destruct32 : Πc2.ΠP:Prop.ch_U = c2 → match c2 with [ ch_U ⇒ P → P | _ ⇒ P ].
 248  #c2; #P; ncases c2; nnormalize;
 249  ##[ ##32: #H; napply (λx:P.x)
 250  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 251  ##]
 252 nqed.
 253
 254 ndefinition ascii_destruct33 : Πc2.ΠP:Prop.ch_V = c2 → match c2 with [ ch_V ⇒ P → P | _ ⇒ P ].
 255  #c2; #P; ncases c2; nnormalize;
 256  ##[ ##33: #H; napply (λx:P.x)
 257  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 258  ##]
 259 nqed.
 260
 261 ndefinition ascii_destruct34 : Πc2.ΠP:Prop.ch_W = c2 → match c2 with [ ch_W ⇒ P → P | _ ⇒ P ].
 262  #c2; #P; ncases c2; nnormalize;
 263  ##[ ##34: #H; napply (λx:P.x)
 264  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 265  ##]
 266 nqed.
 267
 268 ndefinition ascii_destruct35 : Πc2.ΠP:Prop.ch_X = c2 → match c2 with [ ch_X ⇒ P → P | _ ⇒ P ].
 269  #c2; #P; ncases c2; nnormalize;
 270  ##[ ##35: #H; napply (λx:P.x)
 271  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 272  ##]
 273 nqed.
 274
 275 ndefinition ascii_destruct36 : Πc2.ΠP:Prop.ch_Y = c2 → match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ].
 276  #c2; #P; ncases c2; nnormalize;
 277  ##[ ##36: #H; napply (λx:P.x)
 278  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 279  ##]
 280 nqed.
 281
 282 ndefinition ascii_destruct37 : Πc2.ΠP:Prop.ch_Z = c2 → match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ].
 283  #c2; #P; ncases c2; nnormalize;
 284  ##[ ##37: #H; napply (λx:P.x)
 285  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 286  ##]
 287 nqed.
 288
 289 ndefinition ascii_destruct38 : Πc2.ΠP:Prop.ch_a = c2 → match c2 with [ ch_a ⇒ P → P | _ ⇒ P ].
 290  #c2; #P; ncases c2; nnormalize;
 291  ##[ ##38: #H; napply (λx:P.x)
 292  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 293  ##]
 294 nqed.
 295
 296 ndefinition ascii_destruct39 : Πc2.ΠP:Prop.ch_b = c2 → match c2 with [ ch_b ⇒ P → P | _ ⇒ P ].
 297  #c2; #P; ncases c2; nnormalize;
 298  ##[ ##39: #H; napply (λx:P.x)
 299  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 300  ##]
 301 nqed.
 302
 303 ndefinition ascii_destruct40 : Πc2.ΠP:Prop.ch_c = c2 → match c2 with [ ch_c ⇒ P → P | _ ⇒ P ].
 304  #c2; #P; ncases c2; nnormalize;
 305  ##[ ##40: #H; napply (λx:P.x)
 306  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 307  ##]
 308 nqed.
 309
 310 ndefinition ascii_destruct41 : Πc2.ΠP:Prop.ch_d = c2 → match c2 with [ ch_d ⇒ P → P | _ ⇒ P ].
 311  #c2; #P; ncases c2; nnormalize;
 312  ##[ ##41: #H; napply (λx:P.x)
 313  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 314  ##]
 315 nqed.
 316
 317 ndefinition ascii_destruct42 : Πc2.ΠP:Prop.ch_e = c2 → match c2 with [ ch_e ⇒ P → P | _ ⇒ P ].
 318  #c2; #P; ncases c2; nnormalize;
 319  ##[ ##42: #H; napply (λx:P.x)
 320  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 321  ##]
 322 nqed.
 323
 324 ndefinition ascii_destruct43 : Πc2.ΠP:Prop.ch_f = c2 → match c2 with [ ch_f ⇒ P → P | _ ⇒ P ].
 325  #c2; #P; ncases c2; nnormalize;
 326  ##[ ##43: #H; napply (λx:P.x)
 327  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 328  ##]
 329 nqed.
 330
 331 ndefinition ascii_destruct44 : Πc2.ΠP:Prop.ch_g = c2 → match c2 with [ ch_g ⇒ P → P | _ ⇒ P ].
 332  #c2; #P; ncases c2; nnormalize;
 333  ##[ ##44: #H; napply (λx:P.x)
 334  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 335  ##]
 336 nqed.
 337
 338 ndefinition ascii_destruct45 : Πc2.ΠP:Prop.ch_h = c2 → match c2 with [ ch_h ⇒ P → P | _ ⇒ P ].
 339  #c2; #P; ncases c2; nnormalize;
 340  ##[ ##45: #H; napply (λx:P.x)
 341  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 342  ##]
 343 nqed.
 344
 345 ndefinition ascii_destruct46 : Πc2.ΠP:Prop.ch_i = c2 → match c2 with [ ch_i ⇒ P → P | _ ⇒ P ].
 346  #c2; #P; ncases c2; nnormalize;
 347  ##[ ##46: #H; napply (λx:P.x)
 348  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 349  ##]
 350 nqed.
 351
 352 ndefinition ascii_destruct47 : Πc2.ΠP:Prop.ch_j = c2 → match c2 with [ ch_j ⇒ P → P | _ ⇒ P ].
 353  #c2; #P; ncases c2; nnormalize;
 354  ##[ ##47: #H; napply (λx:P.x)
 355  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 356  ##]
 357 nqed.
 358
 359 ndefinition ascii_destruct48 : Πc2.ΠP:Prop.ch_k = c2 → match c2 with [ ch_k ⇒ P → P | _ ⇒ P ].
 360  #c2; #P; ncases c2; nnormalize;
 361  ##[ ##48: #H; napply (λx:P.x)
 362  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 363  ##]
 364 nqed.
 365
 366 ndefinition ascii_destruct49 : Πc2.ΠP:Prop.ch_l = c2 → match c2 with [ ch_l ⇒ P → P | _ ⇒ P ].
 367  #c2; #P; ncases c2; nnormalize;
 368  ##[ ##49: #H; napply (λx:P.x)
 369  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 370  ##]
 371 nqed.
 372
 373 ndefinition ascii_destruct50 : Πc2.ΠP:Prop.ch_m = c2 → match c2 with [ ch_m ⇒ P → P | _ ⇒ P ].
 374  #c2; #P; ncases c2; nnormalize;
 375  ##[ ##50: #H; napply (λx:P.x)
 376  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 377  ##]
 378 nqed.
 379
 380 ndefinition ascii_destruct51 : Πc2.ΠP:Prop.ch_n = c2 → match c2 with [ ch_n ⇒ P → P | _ ⇒ P ].
 381  #c2; #P; ncases c2; nnormalize;
 382  ##[ ##51: #H; napply (λx:P.x)
 383  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 384  ##]
 385 nqed.
 386
 387 ndefinition ascii_destruct52 : Πc2.ΠP:Prop.ch_o = c2 → match c2 with [ ch_o ⇒ P → P | _ ⇒ P ].
 388  #c2; #P; ncases c2; nnormalize;
 389  ##[ ##52: #H; napply (λx:P.x)
 390  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 391  ##]
 392 nqed.
 393
 394 ndefinition ascii_destruct53 : Πc2.ΠP:Prop.ch_p = c2 → match c2 with [ ch_p ⇒ P → P | _ ⇒ P ].
 395  #c2; #P; ncases c2; nnormalize;
 396  ##[ ##53: #H; napply (λx:P.x)
 397  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 398  ##]
 399 nqed.
 400
 401 ndefinition ascii_destruct54 : Πc2.ΠP:Prop.ch_q = c2 → match c2 with [ ch_q ⇒ P → P | _ ⇒ P ].
 402  #c2; #P; ncases c2; nnormalize;
 403  ##[ ##54: #H; napply (λx:P.x)
 404  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 405  ##]
 406 nqed.
 407
 408 ndefinition ascii_destruct55 : Πc2.ΠP:Prop.ch_r = c2 → match c2 with [ ch_r ⇒ P → P | _ ⇒ P ].
 409  #c2; #P; ncases c2; nnormalize;
 410  ##[ ##55: #H; napply (λx:P.x)
 411  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 412  ##]
 413 nqed.
 414
 415 ndefinition ascii_destruct56 : Πc2.ΠP:Prop.ch_s = c2 → match c2 with [ ch_s ⇒ P → P | _ ⇒ P ].
 416  #c2; #P; ncases c2; nnormalize;
 417  ##[ ##56: #H; napply (λx:P.x)
 418  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 419  ##]
 420 nqed.
 421
 422 ndefinition ascii_destruct57 : Πc2.ΠP:Prop.ch_t = c2 → match c2 with [ ch_t ⇒ P → P | _ ⇒ P ].
 423  #c2; #P; ncases c2; nnormalize;
 424  ##[ ##57: #H; napply (λx:P.x)
 425  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 426  ##]
 427 nqed.
 428
 429 ndefinition ascii_destruct58 : Πc2.ΠP:Prop.ch_u = c2 → match c2 with [ ch_u ⇒ P → P | _ ⇒ P ].
 430  #c2; #P; ncases c2; nnormalize;
 431  ##[ ##58: #H; napply (λx:P.x)
 432  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 433  ##]
 434 nqed.
 435
 436 ndefinition ascii_destruct59 : Πc2.ΠP:Prop.ch_v = c2 → match c2 with [ ch_v ⇒ P → P | _ ⇒ P ].
 437  #c2; #P; ncases c2; nnormalize;
 438  ##[ ##59: #H; napply (λx:P.x)
 439  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 440  ##]
 441 nqed.
 442
 443 ndefinition ascii_destruct60 : Πc2.ΠP:Prop.ch_w = c2 → match c2 with [ ch_w ⇒ P → P | _ ⇒ P ].
 444  #c2; #P; ncases c2; nnormalize;
 445  ##[ ##60: #H; napply (λx:P.x)
 446  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 447  ##]
 448 nqed.
 449
 450 ndefinition ascii_destruct61 : Πc2.ΠP:Prop.ch_x = c2 → match c2 with [ ch_x ⇒ P → P | _ ⇒ P ].
 451  #c2; #P; ncases c2; nnormalize;
 452  ##[ ##61: #H; napply (λx:P.x)
 453  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 454  ##]
 455 nqed.
 456
 457 ndefinition ascii_destruct62 : Πc2.ΠP:Prop.ch_y = c2 → match c2 with [ ch_y ⇒ P → P | _ ⇒ P ].
 458  #c2; #P; ncases c2; nnormalize;
 459  ##[ ##62: #H; napply (λx:P.x)
 460  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 461  ##]
 462 nqed.
 463
 464 ndefinition ascii_destruct63 : Πc2.ΠP:Prop.ch_z = c2 → match c2 with [ ch_z ⇒ P → P | _ ⇒ P ].
 465  #c2; #P; ncases c2; nnormalize;
 466  ##[ ##63: #H; napply (λx:P.x)
 467  ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
 468  ##]
 469 nqed.
 470
 471 ndefinition ascii_destruct_aux ≝
 472 Πc1,c2.ΠP:Prop.c1 = c2 →
 473  match c1 with
 474   [ ch_0 ⇒ match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ] | ch_1 ⇒ match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ]
 475   | ch_2 ⇒ match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ] | ch_3 ⇒ match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ]
 476   | ch_4 ⇒ match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ] | ch_5 ⇒ match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ]
 477   | ch_6 ⇒ match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ] | ch_7 ⇒ match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ]
 478   | ch_8 ⇒ match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ] | ch_9 ⇒ match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ]
 479   | ch__ ⇒ match c2 with [ ch__ ⇒ P → P | _ ⇒ P ] | ch_A ⇒ match c2 with [ ch_A ⇒ P → P | _ ⇒ P ]
 480   | ch_B ⇒ match c2 with [ ch_B ⇒ P → P | _ ⇒ P ] | ch_C ⇒ match c2 with [ ch_C ⇒ P → P | _ ⇒ P ]
 481   | ch_D ⇒ match c2 with [ ch_D ⇒ P → P | _ ⇒ P ] | ch_E ⇒ match c2 with [ ch_E ⇒ P → P | _ ⇒ P ]
 482   | ch_F ⇒ match c2 with [ ch_F ⇒ P → P | _ ⇒ P ] | ch_G ⇒ match c2 with [ ch_G ⇒ P → P | _ ⇒ P ]
 483   | ch_H ⇒ match c2 with [ ch_H ⇒ P → P | _ ⇒ P ] | ch_I ⇒ match c2 with [ ch_I ⇒ P → P | _ ⇒ P ]
 484   | ch_J ⇒ match c2 with [ ch_J ⇒ P → P | _ ⇒ P ] | ch_K ⇒ match c2 with [ ch_K ⇒ P → P | _ ⇒ P ]
 485   | ch_L ⇒ match c2 with [ ch_L ⇒ P → P | _ ⇒ P ] | ch_M ⇒ match c2 with [ ch_M ⇒ P → P | _ ⇒ P ]
 486   | ch_N ⇒ match c2 with [ ch_N ⇒ P → P | _ ⇒ P ] | ch_O ⇒ match c2 with [ ch_O ⇒ P → P | _ ⇒ P ]
 487   | ch_P ⇒ match c2 with [ ch_P ⇒ P → P | _ ⇒ P ] | ch_Q ⇒ match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ]
 488   | ch_R ⇒ match c2 with [ ch_R ⇒ P → P | _ ⇒ P ] | ch_S ⇒ match c2 with [ ch_S ⇒ P → P | _ ⇒ P ]
 489   | ch_T ⇒ match c2 with [ ch_T ⇒ P → P | _ ⇒ P ] | ch_U ⇒ match c2 with [ ch_U ⇒ P → P | _ ⇒ P ]
 490   | ch_V ⇒ match c2 with [ ch_V ⇒ P → P | _ ⇒ P ] | ch_W ⇒ match c2 with [ ch_W ⇒ P → P | _ ⇒ P ]
 491   | ch_X ⇒ match c2 with [ ch_X ⇒ P → P | _ ⇒ P ] | ch_Y ⇒ match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ]
 492   | ch_Z ⇒ match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ] | ch_a ⇒ match c2 with [ ch_a ⇒ P → P | _ ⇒ P ]
 493   | ch_b ⇒ match c2 with [ ch_b ⇒ P → P | _ ⇒ P ] | ch_c ⇒ match c2 with [ ch_c ⇒ P → P | _ ⇒ P ]
 494   | ch_d ⇒ match c2 with [ ch_d ⇒ P → P | _ ⇒ P ] | ch_e ⇒ match c2 with [ ch_e ⇒ P → P | _ ⇒ P ]
 495   | ch_f ⇒ match c2 with [ ch_f ⇒ P → P | _ ⇒ P ] | ch_g ⇒ match c2 with [ ch_g ⇒ P → P | _ ⇒ P ]
 496   | ch_h ⇒ match c2 with [ ch_h ⇒ P → P | _ ⇒ P ] | ch_i ⇒ match c2 with [ ch_i ⇒ P → P | _ ⇒ P ]
 497   | ch_j ⇒ match c2 with [ ch_j ⇒ P → P | _ ⇒ P ] | ch_k ⇒ match c2 with [ ch_k ⇒ P → P | _ ⇒ P ]
 498   | ch_l ⇒ match c2 with [ ch_l ⇒ P → P | _ ⇒ P ] | ch_m ⇒ match c2 with [ ch_m ⇒ P → P | _ ⇒ P ]
 499   | ch_n ⇒ match c2 with [ ch_n ⇒ P → P | _ ⇒ P ] | ch_o ⇒ match c2 with [ ch_o ⇒ P → P | _ ⇒ P ]
 500   | ch_p ⇒ match c2 with [ ch_p ⇒ P → P | _ ⇒ P ] | ch_q ⇒ match c2 with [ ch_q ⇒ P → P | _ ⇒ P ]
 501   | ch_r ⇒ match c2 with [ ch_r ⇒ P → P | _ ⇒ P ] | ch_s ⇒ match c2 with [ ch_s ⇒ P → P | _ ⇒ P ]
 502   | ch_t ⇒ match c2 with [ ch_t ⇒ P → P | _ ⇒ P ] | ch_u ⇒ match c2 with [ ch_u ⇒ P → P | _ ⇒ P ]
 503   | ch_v ⇒ match c2 with [ ch_v ⇒ P → P | _ ⇒ P ] | ch_w ⇒ match c2 with [ ch_w ⇒ P → P | _ ⇒ P ]
 504   | ch_x ⇒ match c2 with [ ch_x ⇒ P → P | _ ⇒ P ] | ch_y ⇒ match c2 with [ ch_y ⇒ P → P | _ ⇒ P ]
 505   | ch_z ⇒ match c2 with [ ch_z ⇒ P → P | _ ⇒ P ]].
 506
 507 nlemma ascii_destruct : ascii_destruct_aux.
 508  #c1; ncases c1;
 509  ##[ ##1: napply ascii_destruct1 ##| ##2: napply ascii_destruct2
 510  ##| ##3: napply ascii_destruct3 ##| ##4: napply ascii_destruct4
 511  ##| ##5: napply ascii_destruct5 ##| ##6: napply ascii_destruct6
 512  ##| ##7: napply ascii_destruct7 ##| ##8: napply ascii_destruct8
 513  ##| ##9: napply ascii_destruct9 ##| ##10: napply ascii_destruct10
 514  ##| ##11: napply ascii_destruct11 ##| ##12: napply ascii_destruct12
 515  ##| ##13: napply ascii_destruct13 ##| ##14: napply ascii_destruct14
 516  ##| ##15: napply ascii_destruct15 ##| ##16: napply ascii_destruct16
 517  ##| ##17: napply ascii_destruct17 ##| ##18: napply ascii_destruct18
 518  ##| ##19: napply ascii_destruct19 ##| ##20: napply ascii_destruct20
 519  ##| ##21: napply ascii_destruct21 ##| ##22: napply ascii_destruct22
 520  ##| ##23: napply ascii_destruct23 ##| ##24: napply ascii_destruct24
 521  ##| ##25: napply ascii_destruct25 ##| ##26: napply ascii_destruct26
 522  ##| ##27: napply ascii_destruct27 ##| ##28: napply ascii_destruct28
 523  ##| ##29: napply ascii_destruct29 ##| ##30: napply ascii_destruct30
 524  ##| ##31: napply ascii_destruct31 ##| ##32: napply ascii_destruct32
 525  ##| ##33: napply ascii_destruct33 ##| ##34: napply ascii_destruct34
 526  ##| ##35: napply ascii_destruct35 ##| ##36: napply ascii_destruct36
 527  ##| ##37: napply ascii_destruct37 ##| ##38: napply ascii_destruct38
 528  ##| ##39: napply ascii_destruct39 ##| ##40: napply ascii_destruct40
 529  ##| ##41: napply ascii_destruct41 ##| ##42: napply ascii_destruct42
 530  ##| ##43: napply ascii_destruct43 ##| ##44: napply ascii_destruct44
 531  ##| ##45: napply ascii_destruct45 ##| ##46: napply ascii_destruct46
 532  ##| ##47: napply ascii_destruct47 ##| ##48: napply ascii_destruct48
 533  ##| ##49: napply ascii_destruct49 ##| ##50: napply ascii_destruct50
 534  ##| ##51: napply ascii_destruct51 ##| ##52: napply ascii_destruct52
 535  ##| ##53: napply ascii_destruct53 ##| ##54: napply ascii_destruct54
 536  ##| ##55: napply ascii_destruct55 ##| ##56: napply ascii_destruct56
 537  ##| ##57: napply ascii_destruct57 ##| ##58: napply ascii_destruct58
 538  ##| ##59: napply ascii_destruct59 ##| ##60: napply ascii_destruct60
 539  ##| ##61: napply ascii_destruct61 ##| ##62: napply ascii_destruct62
 540  ##| ##63: napply ascii_destruct63 ##]
 541 nqed.