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

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/exadecim.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* *********** *)
  27 (* ESADECIMALI *)
  28 (* *********** *)
  29
  30 ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
  31  #e2; #P; ncases e2; nnormalize; #H;
  32  ##[ ##1: napply (λx:P.x)
  33  ##| ##*: napply False_ind;
  34           nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
  35           nrewrite > H; nnormalize; napply I
  36  ##]
  37 nqed.
  38
  39 ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
  40  #e2; #P; ncases e2; nnormalize; #H;
  41  ##[ ##2: napply (λx:P.x)
  42  ##| ##*: napply False_ind;
  43           nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
  44           nrewrite > H; nnormalize; napply I
  45  ##]
  46 nqed.
  47
  48 ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
  49  #e2; #P; ncases e2; nnormalize; #H;
  50  ##[ ##3: napply (λx:P.x)
  51  ##| ##*: napply False_ind;
  52           nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
  53           nrewrite > H; nnormalize; napply I
  54  ##]
  55 nqed.
  56
  57 ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
  58  #e2; #P; ncases e2; nnormalize; #H;
  59  ##[ ##4: napply (λx:P.x)
  60  ##| ##*: napply False_ind;
  61           nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
  62           nrewrite > H; nnormalize; napply I
  63  ##]
  64 nqed.
  65
  66 ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
  67  #e2; #P; ncases e2; nnormalize; #H;
  68  ##[ ##5: napply (λx:P.x)
  69  ##| ##*: napply False_ind;
  70           nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
  71           nrewrite > H; nnormalize; napply I
  72  ##]
  73 nqed.
  74
  75 ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
  76  #e2; #P; ncases e2; nnormalize; #H;
  77  ##[ ##6: napply (λx:P.x)
  78  ##| ##*: napply False_ind;
  79           nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
  80           nrewrite > H; nnormalize; napply I
  81  ##]
  82 nqed.
  83
  84 ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
  85  #e2; #P; ncases e2; nnormalize; #H;
  86  ##[ ##7: napply (λx:P.x)
  87  ##| ##*: napply False_ind;
  88           nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
  89           nrewrite > H; nnormalize; napply I
  90  ##]
  91 nqed.
  92
  93 ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
  94  #e2; #P; ncases e2; nnormalize; #H;
  95  ##[ ##8: napply (λx:P.x)
  96  ##| ##*: napply False_ind;
  97           nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
  98           nrewrite > H; nnormalize; napply I
  99  ##]
 100 nqed.
 101
 102 ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
 103  #e2; #P; ncases e2; nnormalize; #H;
 104  ##[ ##9: napply (λx:P.x)
 105  ##| ##*: napply False_ind;
 106           nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
 107           nrewrite > H; nnormalize; napply I
 108  ##]
 109 nqed.
 110
 111 ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
 112  #e2; #P; ncases e2; nnormalize; #H;
 113  ##[ ##10: napply (λx:P.x)
 114  ##| ##*: napply False_ind;
 115           nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
 116           nrewrite > H; nnormalize; napply I
 117  ##]
 118 nqed.
 119
 120 ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
 121  #e2; #P; ncases e2; nnormalize; #H;
 122  ##[ ##11: napply (λx:P.x)
 123  ##| ##*: napply False_ind;
 124           nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
 125           nrewrite > H; nnormalize; napply I
 126  ##]
 127 nqed.
 128
 129 ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
 130  #e2; #P; ncases e2; nnormalize; #H;
 131  ##[ ##12: napply (λx:P.x)
 132  ##| ##*: napply False_ind;
 133           nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
 134           nrewrite > H; nnormalize; napply I
 135  ##]
 136 nqed.
 137
 138 ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
 139  #e2; #P; ncases e2; nnormalize; #H;
 140  ##[ ##13: napply (λx:P.x)
 141  ##| ##*: napply False_ind;
 142           nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
 143           nrewrite > H; nnormalize; napply I
 144  ##]
 145 nqed.
 146
 147 ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
 148  #e2; #P; ncases e2; nnormalize; #H;
 149  ##[ ##14: napply (λx:P.x)
 150  ##| ##*: napply False_ind;
 151           nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
 152           nrewrite > H; nnormalize; napply I
 153  ##]
 154 nqed.
 155
 156 ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
 157  #e2; #P; ncases e2; nnormalize; #H;
 158  ##[ ##15: napply (λx:P.x)
 159  ##| ##*: napply False_ind;
 160           nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
 161           nrewrite > H; nnormalize; napply I
 162  ##]
 163 nqed.
 164
 165 ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
 166  #e2; #P; ncases e2; nnormalize; #H;
 167  ##[ ##16: napply (λx:P.x)
 168  ##| ##*: napply False_ind;
 169           nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
 170           nrewrite > H; nnormalize; napply I
 171  ##]
 172 nqed.
 173
 174 ndefinition exadecim_destruct_aux ≝
 175 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
 176  match e1 with
 177   [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
 178   | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
 179   | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
 180   | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
 181   | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
 182   | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
 183   | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
 184   | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
 185   | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
 186   | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
 187   | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
 188   | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
 189   | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
 190   | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
 191   | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
 192   | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
 193   ].
 194
 195 ndefinition exadecim_destruct : exadecim_destruct_aux.
 196  #e1; ncases e1;
 197  ##[ ##1: napply exadecim_destruct1
 198  ##| ##2: napply exadecim_destruct2
 199  ##| ##3: napply exadecim_destruct3
 200  ##| ##4: napply exadecim_destruct4
 201  ##| ##5: napply exadecim_destruct5
 202  ##| ##6: napply exadecim_destruct6
 203  ##| ##7: napply exadecim_destruct7
 204  ##| ##8: napply exadecim_destruct8
 205  ##| ##9: napply exadecim_destruct9
 206  ##| ##10: napply exadecim_destruct10
 207  ##| ##11: napply exadecim_destruct11
 208  ##| ##12: napply exadecim_destruct12
 209  ##| ##13: napply exadecim_destruct13
 210  ##| ##14: napply exadecim_destruct14
 211  ##| ##15: napply exadecim_destruct15
 212  ##| ##16: napply exadecim_destruct16
 213  ##]
 214 nqed.
 215
 216 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
 217  #e1; #e2;
 218  nelim e1;
 219  nelim e2;
 220  nnormalize;
 221  napply refl_eq.
 222 nqed.
 223
 224 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
 225  #e1; #e2;
 226  nelim e1;
 227  nelim e2;
 228  nnormalize;
 229  napply refl_eq.
 230 nqed.
 231
 232 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
 233  #e1; #e2; #e3;
 234  nelim e1;
 235  ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
 236  ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
 237  ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
 238  ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
 239  ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
 240  ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
 241  ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
 242  ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
 243  ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
 244  ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
 245  ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
 246  ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
 247  ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
 248  ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
 249  ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
 250  ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
 251  ##]
 252 nqed.
 253
 254 nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
 255  #e1; #e2;
 256  nelim e1;
 257  nelim e2;
 258  nnormalize;
 259  napply refl_eq.
 260 nqed.
 261
 262 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
 263  #e1; #e2; #e3;
 264  nelim e1;
 265  ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
 266  ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
 267  ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
 268  ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
 269  ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
 270  ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
 271  ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
 272  ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
 273  ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
 274  ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
 275  ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
 276  ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
 277  ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
 278  ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
 279  ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
 280  ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
 281  ##]
 282 nqed.
 283
 284 nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
 285  #e1; #e2;
 286  nelim e1;
 287  nelim e2;
 288  nnormalize;
 289  napply refl_eq.
 290 nqed.
 291
 292 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
 293  #e1; #e2; #e3;
 294  nelim e1;
 295  ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
 296  ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
 297  ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
 298  ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
 299  ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
 300  ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
 301  ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
 302  ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
 303  ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
 304  ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
 305  ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
 306  ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
 307  ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
 308  ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
 309  ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
 310  ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
 311  ##]
 312 nqed.
 313
 314 nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
 315  #e1; #e2; #c;
 316  nelim e1;
 317  nelim e2;
 318  nelim c;
 319  nnormalize;
 320  napply refl_eq.
 321 nqed.
 322
 323 nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
 324  #e1; #e2; #c;
 325  nelim e1;
 326  nelim e2;
 327  nelim c;
 328  nnormalize;
 329  napply refl_eq.
 330 nqed.
 331
 332 nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
 333  #e1; #e2; #c;
 334  nelim e1;
 335  nelim e2;
 336  nelim c;
 337  nnormalize;
 338  napply refl_eq.
 339 nqed.
 340
 341 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
 342  #e1; #e2;
 343  nelim e1;
 344  nelim e2;
 345  nnormalize;
 346  napply refl_eq.
 347 nqed.
 348
 349 nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
 350  #e1; #e2;
 351  nelim e1;
 352  nelim e2;
 353  nnormalize;
 354  napply refl_eq.
 355 nqed.
 356
 357 nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
 358  #e1; #e2;
 359  nelim e1;
 360  nelim e2;
 361  nnormalize;
 362  napply refl_eq.
 363 nqed.
 364
 365 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
 366  #e1; #e2; #c;
 367  nelim e1;
 368  nelim e2;
 369  nelim c;
 370  nnormalize;
 371  napply refl_eq.
 372 nqed.
 373
 374 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
 375  #e1; #e2; #c;
 376  nelim e1;
 377  nelim e2;
 378  nelim c;
 379  nnormalize;
 380  napply refl_eq.
 381 nqed.
 382
 383 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
 384  #e1; #e2;
 385  nelim e1;
 386  nelim e2;
 387  nnormalize;
 388  napply refl_eq.
 389 nqed.
 390
 391 nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
 392  #e1; #e2;
 393  nelim e1;
 394  nelim e2;
 395  nnormalize;
 396  napply refl_eq.
 397 nqed.
 398
 399 nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
 400  #e1; #e2;
 401  nelim e1;
 402  nelim e2;
 403  nnormalize;
 404  napply refl_eq.
 405 nqed.
 406
 407 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
 408  #e1; #e2;
 409  nelim e1;
 410  nelim e2;
 411  nnormalize;
 412  napply refl_eq.
 413 nqed.
 414
 415 nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
 416  #e1; #e2; #e3;
 417  nelim e1;
 418  ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
 419  ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
 420  ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
 421  ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
 422  ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
 423  ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
 424  ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
 425  ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
 426  ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
 427  ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
 428  ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
 429  ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
 430  ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
 431  ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
 432  ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
 433  ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
 434  ##]
 435 nqed.
 436
 437 nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 438  #e1; #e2;
 439  nelim e1;
 440  nelim e2;
 441  nnormalize;
 442  napply refl_eq.
 443 nqed.
 444
 445 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
 446  #e1; #e2;
 447  ncases e1;
 448  ncases e2;
 449  nnormalize;
 450  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
 451  ##| ##*: #H; napply (bool_destruct … H)
 452  ##]
 453 nqed.
 454
 455 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
 456  #m1; #m2;
 457  ncases m1;
 458  ncases m2;
 459  nnormalize;
 460  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
 461  ##| ##*: #H; napply (exadecim_destruct … H)
 462  ##]
 463 nqed.