helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/opcode_base_lemmas_opcode1.ma".
  28
  29 (* ********************************************** *)
  30 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
  31 (* ********************************************** *)
  32
  33 nlemma symmetric_eqop1 : ∀op2.eq_op ADC op2 = eq_op op2 ADC. #op2; nnormalize; napply (refl_eq ??).nqed.
  34 nlemma symmetric_eqop2 : ∀op2.eq_op ADD op2 = eq_op op2 ADD. #op2; nnormalize; napply (refl_eq ??).nqed.
  35 nlemma symmetric_eqop3 : ∀op2.eq_op AIS op2 = eq_op op2 AIS. #op2; nnormalize; napply (refl_eq ??).nqed.
  36 nlemma symmetric_eqop4 : ∀op2.eq_op AIX op2 = eq_op op2 AIX. #op2; nnormalize; napply (refl_eq ??).nqed.
  37 nlemma symmetric_eqop5 : ∀op2.eq_op AND op2 = eq_op op2 AND. #op2; nnormalize; napply (refl_eq ??).nqed.
  38 nlemma symmetric_eqop6 : ∀op2.eq_op ASL op2 = eq_op op2 ASL. #op2; nnormalize; napply (refl_eq ??).nqed.
  39 nlemma symmetric_eqop7 : ∀op2.eq_op ASR op2 = eq_op op2 ASR. #op2; nnormalize; napply (refl_eq ??).nqed.
  40 nlemma symmetric_eqop8 : ∀op2.eq_op BCC op2 = eq_op op2 BCC. #op2; nnormalize; napply (refl_eq ??).nqed.
  41 nlemma symmetric_eqop9 : ∀op2.eq_op BCLRn op2 = eq_op op2 BCLRn. #op2; nnormalize; napply (refl_eq ??).nqed.
  42 nlemma symmetric_eqop10 : ∀op2.eq_op BCS op2 = eq_op op2 BCS. #op2; nnormalize; napply (refl_eq ??).nqed.
  43 nlemma symmetric_eqop11 : ∀op2.eq_op BEQ op2 = eq_op op2 BEQ. #op2; nnormalize; napply (refl_eq ??).nqed.
  44 nlemma symmetric_eqop12 : ∀op2.eq_op BGE op2 = eq_op op2 BGE. #op2; nnormalize; napply (refl_eq ??).nqed.
  45 nlemma symmetric_eqop13 : ∀op2.eq_op BGND op2 = eq_op op2 BGND. #op2; nnormalize; napply (refl_eq ??).nqed.
  46 nlemma symmetric_eqop14 : ∀op2.eq_op BGT op2 = eq_op op2 BGT. #op2; nnormalize; napply (refl_eq ??).nqed.
  47 nlemma symmetric_eqop15 : ∀op2.eq_op BHCC op2 = eq_op op2 BHCC. #op2; nnormalize; napply (refl_eq ??).nqed.
  48 nlemma symmetric_eqop16 : ∀op2.eq_op BHCS op2 = eq_op op2 BHCS. #op2; nnormalize; napply (refl_eq ??).nqed.
  49 nlemma symmetric_eqop17 : ∀op2.eq_op BHI op2 = eq_op op2 BHI. #op2; nnormalize; napply (refl_eq ??).nqed.
  50 nlemma symmetric_eqop18 : ∀op2.eq_op BIH op2 = eq_op op2 BIH. #op2; nnormalize; napply (refl_eq ??).nqed.
  51 nlemma symmetric_eqop19 : ∀op2.eq_op BIL op2 = eq_op op2 BIL. #op2; nnormalize; napply (refl_eq ??).nqed.
  52 nlemma symmetric_eqop20 : ∀op2.eq_op BIT op2 = eq_op op2 BIT. #op2; nnormalize; napply (refl_eq ??).nqed.
  53 nlemma symmetric_eqop21 : ∀op2.eq_op BLE op2 = eq_op op2 BLE. #op2; nnormalize; napply (refl_eq ??).nqed.
  54 nlemma symmetric_eqop22 : ∀op2.eq_op BLS op2 = eq_op op2 BLS. #op2; nnormalize; napply (refl_eq ??).nqed.
  55 nlemma symmetric_eqop23 : ∀op2.eq_op BLT op2 = eq_op op2 BLT. #op2; nnormalize; napply (refl_eq ??).nqed.
  56 nlemma symmetric_eqop24 : ∀op2.eq_op BMC op2 = eq_op op2 BMC. #op2; nnormalize; napply (refl_eq ??).nqed.
  57 nlemma symmetric_eqop25 : ∀op2.eq_op BMI op2 = eq_op op2 BMI. #op2; nnormalize; napply (refl_eq ??).nqed.
  58 nlemma symmetric_eqop26 : ∀op2.eq_op BMS op2 = eq_op op2 BMS. #op2; nnormalize; napply (refl_eq ??).nqed.
  59 nlemma symmetric_eqop27 : ∀op2.eq_op BNE op2 = eq_op op2 BNE. #op2; nnormalize; napply (refl_eq ??).nqed.
  60 nlemma symmetric_eqop28 : ∀op2.eq_op BPL op2 = eq_op op2 BPL. #op2; nnormalize; napply (refl_eq ??).nqed.
  61 nlemma symmetric_eqop29 : ∀op2.eq_op BRA op2 = eq_op op2 BRA. #op2; nnormalize; napply (refl_eq ??).nqed.
  62 nlemma symmetric_eqop30 : ∀op2.eq_op BRCLRn op2 = eq_op op2 BRCLRn. #op2; nnormalize; napply (refl_eq ??).nqed.
  63 nlemma symmetric_eqop31 : ∀op2.eq_op BRN op2 = eq_op op2 BRN. #op2; nnormalize; napply (refl_eq ??).nqed.
  64 nlemma symmetric_eqop32 : ∀op2.eq_op BRSETn op2 = eq_op op2 BRSETn. #op2; nnormalize; napply (refl_eq ??).nqed.
  65 nlemma symmetric_eqop33 : ∀op2.eq_op BSETn op2 = eq_op op2 BSETn. #op2; nnormalize; napply (refl_eq ??).nqed.
  66 nlemma symmetric_eqop34 : ∀op2.eq_op BSR op2 = eq_op op2 BSR. #op2; nnormalize; napply (refl_eq ??).nqed.
  67 nlemma symmetric_eqop35 : ∀op2.eq_op CBEQA op2 = eq_op op2 CBEQA. #op2; nnormalize; napply (refl_eq ??).nqed.
  68 nlemma symmetric_eqop36 : ∀op2.eq_op CBEQX op2 = eq_op op2 CBEQX. #op2; nnormalize; napply (refl_eq ??).nqed.
  69 nlemma symmetric_eqop37 : ∀op2.eq_op CLC op2 = eq_op op2 CLC. #op2; nnormalize; napply (refl_eq ??).nqed.
  70 nlemma symmetric_eqop38 : ∀op2.eq_op CLI op2 = eq_op op2 CLI. #op2; nnormalize; napply (refl_eq ??).nqed.
  71 nlemma symmetric_eqop39 : ∀op2.eq_op CLR op2 = eq_op op2 CLR. #op2; nnormalize; napply (refl_eq ??).nqed.
  72 nlemma symmetric_eqop40 : ∀op2.eq_op CMP op2 = eq_op op2 CMP. #op2; nnormalize; napply (refl_eq ??).nqed.
  73 nlemma symmetric_eqop41 : ∀op2.eq_op COM op2 = eq_op op2 COM. #op2; nnormalize; napply (refl_eq ??).nqed.
  74 nlemma symmetric_eqop42 : ∀op2.eq_op CPHX op2 = eq_op op2 CPHX. #op2; nnormalize; napply (refl_eq ??).nqed.
  75 nlemma symmetric_eqop43 : ∀op2.eq_op CPX op2 = eq_op op2 CPX. #op2; nnormalize; napply (refl_eq ??).nqed.
  76 nlemma symmetric_eqop44 : ∀op2.eq_op DAA op2 = eq_op op2 DAA. #op2; nnormalize; napply (refl_eq ??).nqed.
  77 nlemma symmetric_eqop45 : ∀op2.eq_op DBNZ op2 = eq_op op2 DBNZ. #op2; nnormalize; napply (refl_eq ??).nqed.
  78 nlemma symmetric_eqop46 : ∀op2.eq_op DEC op2 = eq_op op2 DEC. #op2; nnormalize; napply (refl_eq ??).nqed.
  79 nlemma symmetric_eqop47 : ∀op2.eq_op DIV op2 = eq_op op2 DIV. #op2; nnormalize; napply (refl_eq ??).nqed.
  80 nlemma symmetric_eqop48 : ∀op2.eq_op EOR op2 = eq_op op2 EOR. #op2; nnormalize; napply (refl_eq ??).nqed.
  81 nlemma symmetric_eqop49 : ∀op2.eq_op INC op2 = eq_op op2 INC. #op2; nnormalize; napply (refl_eq ??).nqed.
  82 nlemma symmetric_eqop50 : ∀op2.eq_op JMP op2 = eq_op op2 JMP. #op2; nnormalize; napply (refl_eq ??).nqed.
  83 nlemma symmetric_eqop51 : ∀op2.eq_op JSR op2 = eq_op op2 JSR. #op2; nnormalize; napply (refl_eq ??).nqed.
  84 nlemma symmetric_eqop52 : ∀op2.eq_op LDA op2 = eq_op op2 LDA. #op2; nnormalize; napply (refl_eq ??).nqed.
  85 nlemma symmetric_eqop53 : ∀op2.eq_op LDHX op2 = eq_op op2 LDHX. #op2; nnormalize; napply (refl_eq ??).nqed.
  86 nlemma symmetric_eqop54 : ∀op2.eq_op LDX op2 = eq_op op2 LDX. #op2; nnormalize; napply (refl_eq ??).nqed.
  87 nlemma symmetric_eqop55 : ∀op2.eq_op LSR op2 = eq_op op2 LSR. #op2; nnormalize; napply (refl_eq ??).nqed.
  88 nlemma symmetric_eqop56 : ∀op2.eq_op MOV op2 = eq_op op2 MOV. #op2; nnormalize; napply (refl_eq ??).nqed.
  89 nlemma symmetric_eqop57 : ∀op2.eq_op MUL op2 = eq_op op2 MUL. #op2; nnormalize; napply (refl_eq ??).nqed.
  90 nlemma symmetric_eqop58 : ∀op2.eq_op NEG op2 = eq_op op2 NEG. #op2; nnormalize; napply (refl_eq ??).nqed.
  91 nlemma symmetric_eqop59 : ∀op2.eq_op NOP op2 = eq_op op2 NOP. #op2; nnormalize; napply (refl_eq ??).nqed.
  92 nlemma symmetric_eqop60 : ∀op2.eq_op NSA op2 = eq_op op2 NSA. #op2; nnormalize; napply (refl_eq ??).nqed.
  93 nlemma symmetric_eqop61 : ∀op2.eq_op ORA op2 = eq_op op2 ORA. #op2; nnormalize; napply (refl_eq ??).nqed.
  94 nlemma symmetric_eqop62 : ∀op2.eq_op PSHA op2 = eq_op op2 PSHA. #op2; nnormalize; napply (refl_eq ??).nqed.
  95 nlemma symmetric_eqop63 : ∀op2.eq_op PSHH op2 = eq_op op2 PSHH. #op2; nnormalize; napply (refl_eq ??).nqed.
  96 nlemma symmetric_eqop64 : ∀op2.eq_op PSHX op2 = eq_op op2 PSHX. #op2; nnormalize; napply (refl_eq ??).nqed.
  97 nlemma symmetric_eqop65 : ∀op2.eq_op PULA op2 = eq_op op2 PULA. #op2; nnormalize; napply (refl_eq ??).nqed.
  98 nlemma symmetric_eqop66 : ∀op2.eq_op PULH op2 = eq_op op2 PULH. #op2; nnormalize; napply (refl_eq ??).nqed.
  99 nlemma symmetric_eqop67 : ∀op2.eq_op PULX op2 = eq_op op2 PULX. #op2; nnormalize; napply (refl_eq ??).nqed.
 100 nlemma symmetric_eqop68 : ∀op2.eq_op ROL op2 = eq_op op2 ROL. #op2; nnormalize; napply (refl_eq ??).nqed.
 101 nlemma symmetric_eqop69 : ∀op2.eq_op ROR op2 = eq_op op2 ROR. #op2; nnormalize; napply (refl_eq ??).nqed.
 102 nlemma symmetric_eqop70 : ∀op2.eq_op RSP op2 = eq_op op2 RSP. #op2; nnormalize; napply (refl_eq ??).nqed.
 103 nlemma symmetric_eqop71 : ∀op2.eq_op RTI op2 = eq_op op2 RTI. #op2; nnormalize; napply (refl_eq ??).nqed.
 104 nlemma symmetric_eqop72 : ∀op2.eq_op RTS op2 = eq_op op2 RTS. #op2; nnormalize; napply (refl_eq ??).nqed.
 105 nlemma symmetric_eqop73 : ∀op2.eq_op SBC op2 = eq_op op2 SBC. #op2; nnormalize; napply (refl_eq ??).nqed.
 106 nlemma symmetric_eqop74 : ∀op2.eq_op SEC op2 = eq_op op2 SEC. #op2; nnormalize; napply (refl_eq ??).nqed.
 107 nlemma symmetric_eqop75 : ∀op2.eq_op SEI op2 = eq_op op2 SEI. #op2; nnormalize; napply (refl_eq ??).nqed.
 108 nlemma symmetric_eqop76 : ∀op2.eq_op SHA op2 = eq_op op2 SHA. #op2; nnormalize; napply (refl_eq ??).nqed.
 109 nlemma symmetric_eqop77 : ∀op2.eq_op SLA op2 = eq_op op2 SLA. #op2; nnormalize; napply (refl_eq ??).nqed.
 110 nlemma symmetric_eqop78 : ∀op2.eq_op STA op2 = eq_op op2 STA. #op2; nnormalize; napply (refl_eq ??).nqed.
 111 nlemma symmetric_eqop79 : ∀op2.eq_op STHX op2 = eq_op op2 STHX. #op2; nnormalize; napply (refl_eq ??).nqed.
 112 nlemma symmetric_eqop80 : ∀op2.eq_op STOP op2 = eq_op op2 STOP. #op2; nnormalize; napply (refl_eq ??).nqed.
 113 nlemma symmetric_eqop81 : ∀op2.eq_op STX op2 = eq_op op2 STX. #op2; nnormalize; napply (refl_eq ??).nqed.
 114 nlemma symmetric_eqop82 : ∀op2.eq_op SUB op2 = eq_op op2 SUB. #op2; nnormalize; napply (refl_eq ??).nqed.
 115 nlemma symmetric_eqop83 : ∀op2.eq_op SWI op2 = eq_op op2 SWI. #op2; nnormalize; napply (refl_eq ??).nqed.
 116 nlemma symmetric_eqop84 : ∀op2.eq_op TAP op2 = eq_op op2 TAP. #op2; nnormalize; napply (refl_eq ??).nqed.
 117 nlemma symmetric_eqop85 : ∀op2.eq_op TAX op2 = eq_op op2 TAX. #op2; nnormalize; napply (refl_eq ??).nqed.
 118 nlemma symmetric_eqop86 : ∀op2.eq_op TPA op2 = eq_op op2 TPA. #op2; nnormalize; napply (refl_eq ??).nqed.
 119 nlemma symmetric_eqop87 : ∀op2.eq_op TST op2 = eq_op op2 TST. #op2; nnormalize; napply (refl_eq ??).nqed.
 120 nlemma symmetric_eqop88 : ∀op2.eq_op TSX op2 = eq_op op2 TSX. #op2; nnormalize; napply (refl_eq ??).nqed.
 121 nlemma symmetric_eqop89 : ∀op2.eq_op TXA op2 = eq_op op2 TXA. #op2; nnormalize; napply (refl_eq ??).nqed.
 122 nlemma symmetric_eqop90 : ∀op2.eq_op TXS op2 = eq_op op2 TXS. #op2; nnormalize; napply (refl_eq ??).nqed.
 123 nlemma symmetric_eqop91 : ∀op2.eq_op WAIT op2 = eq_op op2 WAIT. #op2; nnormalize; napply (refl_eq ??).nqed.
 124
 125 nlemma symmetric_eqop : symmetricT opcode bool eq_op.
 126  #op1; ncases op1;
 127  ##[ ##1: napply symmetric_eqop1 ##| ##2: napply symmetric_eqop2 ##| ##3: napply symmetric_eqop3 ##| ##4: napply symmetric_eqop4
 128  ##| ##5: napply symmetric_eqop5 ##| ##6: napply symmetric_eqop6 ##| ##7: napply symmetric_eqop7 ##| ##8: napply symmetric_eqop8
 129  ##| ##9: napply symmetric_eqop9 ##| ##10: napply symmetric_eqop10 ##| ##11: napply symmetric_eqop11 ##| ##12: napply symmetric_eqop12
 130  ##| ##13: napply symmetric_eqop13 ##| ##14: napply symmetric_eqop14 ##| ##15: napply symmetric_eqop15 ##| ##16: napply symmetric_eqop16
 131  ##| ##17: napply symmetric_eqop17 ##| ##18: napply symmetric_eqop18 ##| ##19: napply symmetric_eqop19 ##| ##20: napply symmetric_eqop20
 132  ##| ##21: napply symmetric_eqop21 ##| ##22: napply symmetric_eqop22 ##| ##23: napply symmetric_eqop23 ##| ##24: napply symmetric_eqop24
 133  ##| ##25: napply symmetric_eqop25 ##| ##26: napply symmetric_eqop26 ##| ##27: napply symmetric_eqop27 ##| ##28: napply symmetric_eqop28
 134  ##| ##29: napply symmetric_eqop29 ##| ##30: napply symmetric_eqop30 ##| ##31: napply symmetric_eqop31 ##| ##32: napply symmetric_eqop32
 135  ##| ##33: napply symmetric_eqop33 ##| ##34: napply symmetric_eqop34 ##| ##35: napply symmetric_eqop35 ##| ##36: napply symmetric_eqop36
 136  ##| ##37: napply symmetric_eqop37 ##| ##38: napply symmetric_eqop38 ##| ##39: napply symmetric_eqop39 ##| ##40: napply symmetric_eqop40
 137  ##| ##41: napply symmetric_eqop41 ##| ##42: napply symmetric_eqop42 ##| ##43: napply symmetric_eqop43 ##| ##44: napply symmetric_eqop44
 138  ##| ##45: napply symmetric_eqop45 ##| ##46: napply symmetric_eqop46 ##| ##47: napply symmetric_eqop47 ##| ##48: napply symmetric_eqop48
 139  ##| ##49: napply symmetric_eqop49 ##| ##50: napply symmetric_eqop50 ##| ##51: napply symmetric_eqop51 ##| ##52: napply symmetric_eqop52
 140  ##| ##53: napply symmetric_eqop53 ##| ##54: napply symmetric_eqop54 ##| ##55: napply symmetric_eqop55 ##| ##56: napply symmetric_eqop56
 141  ##| ##57: napply symmetric_eqop57 ##| ##58: napply symmetric_eqop58 ##| ##59: napply symmetric_eqop59 ##| ##60: napply symmetric_eqop60
 142  ##| ##61: napply symmetric_eqop61 ##| ##62: napply symmetric_eqop62 ##| ##63: napply symmetric_eqop63 ##| ##64: napply symmetric_eqop64
 143  ##| ##65: napply symmetric_eqop65 ##| ##66: napply symmetric_eqop66 ##| ##67: napply symmetric_eqop67 ##| ##68: napply symmetric_eqop68
 144  ##| ##69: napply symmetric_eqop69 ##| ##70: napply symmetric_eqop70 ##| ##71: napply symmetric_eqop71 ##| ##72: napply symmetric_eqop72
 145  ##| ##73: napply symmetric_eqop73 ##| ##74: napply symmetric_eqop74 ##| ##75: napply symmetric_eqop75 ##| ##76: napply symmetric_eqop76
 146  ##| ##77: napply symmetric_eqop77 ##| ##78: napply symmetric_eqop78 ##| ##79: napply symmetric_eqop79 ##| ##80: napply symmetric_eqop80
 147  ##| ##81: napply symmetric_eqop81 ##| ##82: napply symmetric_eqop82 ##| ##83: napply symmetric_eqop83 ##| ##84: napply symmetric_eqop84
 148  ##| ##85: napply symmetric_eqop85 ##| ##86: napply symmetric_eqop86 ##| ##87: napply symmetric_eqop87 ##| ##88: napply symmetric_eqop88
 149  ##| ##89: napply symmetric_eqop89 ##| ##90: napply symmetric_eqop90 ##| ##91: napply symmetric_eqop91 ##]
 150 nqed.
 151
 152 nlemma eqop_to_eq1 : ∀op2.eq_op ADC op2 = true → ADC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 153 nlemma eqop_to_eq2 : ∀op2.eq_op ADD op2 = true → ADD = op2. #op2; ncases op2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 154 nlemma eqop_to_eq3 : ∀op2.eq_op AIS op2 = true → AIS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 155 nlemma eqop_to_eq4 : ∀op2.eq_op AIX op2 = true → AIX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 156 nlemma eqop_to_eq5 : ∀op2.eq_op AND op2 = true → AND = op2. #op2; ncases op2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 157 nlemma eqop_to_eq6 : ∀op2.eq_op ASL op2 = true → ASL = op2. #op2; ncases op2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 158 nlemma eqop_to_eq7 : ∀op2.eq_op ASR op2 = true → ASR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 159 nlemma eqop_to_eq8 : ∀op2.eq_op BCC op2 = true → BCC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 160 nlemma eqop_to_eq9 : ∀op2.eq_op BCLRn op2 = true → BCLRn = op2. #op2; ncases op2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 161 nlemma eqop_to_eq10 : ∀op2.eq_op BCS op2 = true → BCS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 162 nlemma eqop_to_eq11 : ∀op2.eq_op BEQ op2 = true → BEQ = op2. #op2; ncases op2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 163 nlemma eqop_to_eq12 : ∀op2.eq_op BGE op2 = true → BGE = op2. #op2; ncases op2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 164 nlemma eqop_to_eq13 : ∀op2.eq_op BGND op2 = true → BGND = op2. #op2; ncases op2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 165 nlemma eqop_to_eq14 : ∀op2.eq_op BGT op2 = true → BGT = op2. #op2; ncases op2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 166 nlemma eqop_to_eq15 : ∀op2.eq_op BHCC op2 = true → BHCC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 167 nlemma eqop_to_eq16 : ∀op2.eq_op BHCS op2 = true → BHCS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 168 nlemma eqop_to_eq17 : ∀op2.eq_op BHI op2 = true → BHI = op2. #op2; ncases op2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 169 nlemma eqop_to_eq18 : ∀op2.eq_op BIH op2 = true → BIH = op2. #op2; ncases op2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 170 nlemma eqop_to_eq19 : ∀op2.eq_op BIL op2 = true → BIL = op2. #op2; ncases op2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 171 nlemma eqop_to_eq20 : ∀op2.eq_op BIT op2 = true → BIT = op2. #op2; ncases op2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 172 nlemma eqop_to_eq21 : ∀op2.eq_op BLE op2 = true → BLE = op2. #op2; ncases op2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 173 nlemma eqop_to_eq22 : ∀op2.eq_op BLS op2 = true → BLS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 174 nlemma eqop_to_eq23 : ∀op2.eq_op BLT op2 = true → BLT = op2. #op2; ncases op2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 175 nlemma eqop_to_eq24 : ∀op2.eq_op BMC op2 = true → BMC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 176 nlemma eqop_to_eq25 : ∀op2.eq_op BMI op2 = true → BMI = op2. #op2; ncases op2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 177 nlemma eqop_to_eq26 : ∀op2.eq_op BMS op2 = true → BMS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 178 nlemma eqop_to_eq27 : ∀op2.eq_op BNE op2 = true → BNE = op2. #op2; ncases op2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 179 nlemma eqop_to_eq28 : ∀op2.eq_op BPL op2 = true → BPL = op2. #op2; ncases op2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 180 nlemma eqop_to_eq29 : ∀op2.eq_op BRA op2 = true → BRA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 181 nlemma eqop_to_eq30 : ∀op2.eq_op BRCLRn op2 = true → BRCLRn = op2. #op2; ncases op2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 182 nlemma eqop_to_eq31 : ∀op2.eq_op BRN op2 = true → BRN = op2. #op2; ncases op2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 183 nlemma eqop_to_eq32 : ∀op2.eq_op BRSETn op2 = true → BRSETn = op2. #op2; ncases op2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 184 nlemma eqop_to_eq33 : ∀op2.eq_op BSETn op2 = true → BSETn = op2. #op2; ncases op2; nnormalize; #H; ##[ ##33: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 185 nlemma eqop_to_eq34 : ∀op2.eq_op BSR op2 = true → BSR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##34: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 186 nlemma eqop_to_eq35 : ∀op2.eq_op CBEQA op2 = true → CBEQA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##35: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 187 nlemma eqop_to_eq36 : ∀op2.eq_op CBEQX op2 = true → CBEQX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##36: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 188 nlemma eqop_to_eq37 : ∀op2.eq_op CLC op2 = true → CLC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##37: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 189 nlemma eqop_to_eq38 : ∀op2.eq_op CLI op2 = true → CLI = op2. #op2; ncases op2; nnormalize; #H; ##[ ##38: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 190 nlemma eqop_to_eq39 : ∀op2.eq_op CLR op2 = true → CLR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##39: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 191 nlemma eqop_to_eq40 : ∀op2.eq_op CMP op2 = true → CMP = op2. #op2; ncases op2; nnormalize; #H; ##[ ##40: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 192 nlemma eqop_to_eq41 : ∀op2.eq_op COM op2 = true → COM = op2. #op2; ncases op2; nnormalize; #H; ##[ ##41: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 193 nlemma eqop_to_eq42 : ∀op2.eq_op CPHX op2 = true → CPHX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##42: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 194 nlemma eqop_to_eq43 : ∀op2.eq_op CPX op2 = true → CPX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##43: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 195 nlemma eqop_to_eq44 : ∀op2.eq_op DAA op2 = true → DAA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##44: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 196 nlemma eqop_to_eq45 : ∀op2.eq_op DBNZ op2 = true → DBNZ = op2. #op2; ncases op2; nnormalize; #H; ##[ ##45: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 197 nlemma eqop_to_eq46 : ∀op2.eq_op DEC op2 = true → DEC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##46: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 198 nlemma eqop_to_eq47 : ∀op2.eq_op DIV op2 = true → DIV = op2. #op2; ncases op2; nnormalize; #H; ##[ ##47: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 199 nlemma eqop_to_eq48 : ∀op2.eq_op EOR op2 = true → EOR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##48: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 200 nlemma eqop_to_eq49 : ∀op2.eq_op INC op2 = true → INC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##49: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 201 nlemma eqop_to_eq50 : ∀op2.eq_op JMP op2 = true → JMP = op2. #op2; ncases op2; nnormalize; #H; ##[ ##50: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 202 nlemma eqop_to_eq51 : ∀op2.eq_op JSR op2 = true → JSR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##51: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 203 nlemma eqop_to_eq52 : ∀op2.eq_op LDA op2 = true → LDA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##52: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 204 nlemma eqop_to_eq53 : ∀op2.eq_op LDHX op2 = true → LDHX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##53: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 205 nlemma eqop_to_eq54 : ∀op2.eq_op LDX op2 = true → LDX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##54: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 206 nlemma eqop_to_eq55 : ∀op2.eq_op LSR op2 = true → LSR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##55: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 207 nlemma eqop_to_eq56 : ∀op2.eq_op MOV op2 = true → MOV = op2. #op2; ncases op2; nnormalize; #H; ##[ ##56: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 208 nlemma eqop_to_eq57 : ∀op2.eq_op MUL op2 = true → MUL = op2. #op2; ncases op2; nnormalize; #H; ##[ ##57: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 209 nlemma eqop_to_eq58 : ∀op2.eq_op NEG op2 = true → NEG = op2. #op2; ncases op2; nnormalize; #H; ##[ ##58: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 210 nlemma eqop_to_eq59 : ∀op2.eq_op NOP op2 = true → NOP = op2. #op2; ncases op2; nnormalize; #H; ##[ ##59: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 211 nlemma eqop_to_eq60 : ∀op2.eq_op NSA op2 = true → NSA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##60: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 212 nlemma eqop_to_eq61 : ∀op2.eq_op ORA op2 = true → ORA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##61: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 213 nlemma eqop_to_eq62 : ∀op2.eq_op PSHA op2 = true → PSHA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##62: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 214 nlemma eqop_to_eq63 : ∀op2.eq_op PSHH op2 = true → PSHH = op2. #op2; ncases op2; nnormalize; #H; ##[ ##63: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 215 nlemma eqop_to_eq64 : ∀op2.eq_op PSHX op2 = true → PSHX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##64: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 216 nlemma eqop_to_eq65 : ∀op2.eq_op PULA op2 = true → PULA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##65: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 217 nlemma eqop_to_eq66 : ∀op2.eq_op PULH op2 = true → PULH = op2. #op2; ncases op2; nnormalize; #H; ##[ ##66: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 218 nlemma eqop_to_eq67 : ∀op2.eq_op PULX op2 = true → PULX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##67: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 219 nlemma eqop_to_eq68 : ∀op2.eq_op ROL op2 = true → ROL = op2. #op2; ncases op2; nnormalize; #H; ##[ ##68: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 220 nlemma eqop_to_eq69 : ∀op2.eq_op ROR op2 = true → ROR = op2. #op2; ncases op2; nnormalize; #H; ##[ ##69: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 221 nlemma eqop_to_eq70 : ∀op2.eq_op RSP op2 = true → RSP = op2. #op2; ncases op2; nnormalize; #H; ##[ ##70: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 222 nlemma eqop_to_eq71 : ∀op2.eq_op RTI op2 = true → RTI = op2. #op2; ncases op2; nnormalize; #H; ##[ ##71: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 223 nlemma eqop_to_eq72 : ∀op2.eq_op RTS op2 = true → RTS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##72: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 224 nlemma eqop_to_eq73 : ∀op2.eq_op SBC op2 = true → SBC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##73: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 225 nlemma eqop_to_eq74 : ∀op2.eq_op SEC op2 = true → SEC = op2. #op2; ncases op2; nnormalize; #H; ##[ ##74: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 226 nlemma eqop_to_eq75 : ∀op2.eq_op SEI op2 = true → SEI = op2. #op2; ncases op2; nnormalize; #H; ##[ ##75: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 227 nlemma eqop_to_eq76 : ∀op2.eq_op SHA op2 = true → SHA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##76: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 228 nlemma eqop_to_eq77 : ∀op2.eq_op SLA op2 = true → SLA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##77: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 229 nlemma eqop_to_eq78 : ∀op2.eq_op STA op2 = true → STA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##78: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 230 nlemma eqop_to_eq79 : ∀op2.eq_op STHX op2 = true → STHX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##79: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 231 nlemma eqop_to_eq80 : ∀op2.eq_op STOP op2 = true → STOP = op2. #op2; ncases op2; nnormalize; #H; ##[ ##80: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 232 nlemma eqop_to_eq81 : ∀op2.eq_op STX op2 = true → STX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##81: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 233 nlemma eqop_to_eq82 : ∀op2.eq_op SUB op2 = true → SUB = op2. #op2; ncases op2; nnormalize; #H; ##[ ##82: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 234 nlemma eqop_to_eq83 : ∀op2.eq_op SWI op2 = true → SWI = op2. #op2; ncases op2; nnormalize; #H; ##[ ##83: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 235 nlemma eqop_to_eq84 : ∀op2.eq_op TAP op2 = true → TAP = op2. #op2; ncases op2; nnormalize; #H; ##[ ##84: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 236 nlemma eqop_to_eq85 : ∀op2.eq_op TAX op2 = true → TAX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##85: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 237 nlemma eqop_to_eq86 : ∀op2.eq_op TPA op2 = true → TPA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##86: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 238 nlemma eqop_to_eq87 : ∀op2.eq_op TST op2 = true → TST = op2. #op2; ncases op2; nnormalize; #H; ##[ ##87: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 239 nlemma eqop_to_eq88 : ∀op2.eq_op TSX op2 = true → TSX = op2. #op2; ncases op2; nnormalize; #H; ##[ ##88: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 240 nlemma eqop_to_eq89 : ∀op2.eq_op TXA op2 = true → TXA = op2. #op2; ncases op2; nnormalize; #H; ##[ ##89: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 241 nlemma eqop_to_eq90 : ∀op2.eq_op TXS op2 = true → TXS = op2. #op2; ncases op2; nnormalize; #H; ##[ ##90: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 242 nlemma eqop_to_eq91 : ∀op2.eq_op WAIT op2 = true → WAIT = op2. #op2; ncases op2; nnormalize; #H; ##[ ##91: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]nqed.
 243
 244 nlemma eqop_to_eq : ∀op1,op2.eq_op op1 op2 = true → op1 = op2.
 245  #op1; ncases op1;
 246  ##[ ##1: napply eqop_to_eq1 ##| ##2: napply eqop_to_eq2 ##| ##3: napply eqop_to_eq3 ##| ##4: napply eqop_to_eq4
 247  ##| ##5: napply eqop_to_eq5 ##| ##6: napply eqop_to_eq6 ##| ##7: napply eqop_to_eq7 ##| ##8: napply eqop_to_eq8
 248  ##| ##9: napply eqop_to_eq9 ##| ##10: napply eqop_to_eq10 ##| ##11: napply eqop_to_eq11 ##| ##12: napply eqop_to_eq12
 249  ##| ##13: napply eqop_to_eq13 ##| ##14: napply eqop_to_eq14 ##| ##15: napply eqop_to_eq15 ##| ##16: napply eqop_to_eq16
 250  ##| ##17: napply eqop_to_eq17 ##| ##18: napply eqop_to_eq18 ##| ##19: napply eqop_to_eq19 ##| ##20: napply eqop_to_eq20
 251  ##| ##21: napply eqop_to_eq21 ##| ##22: napply eqop_to_eq22 ##| ##23: napply eqop_to_eq23 ##| ##24: napply eqop_to_eq24
 252  ##| ##25: napply eqop_to_eq25 ##| ##26: napply eqop_to_eq26 ##| ##27: napply eqop_to_eq27 ##| ##28: napply eqop_to_eq28
 253  ##| ##29: napply eqop_to_eq29 ##| ##30: napply eqop_to_eq30 ##| ##31: napply eqop_to_eq31 ##| ##32: napply eqop_to_eq32
 254  ##| ##33: napply eqop_to_eq33 ##| ##34: napply eqop_to_eq34 ##| ##35: napply eqop_to_eq35 ##| ##36: napply eqop_to_eq36
 255  ##| ##37: napply eqop_to_eq37 ##| ##38: napply eqop_to_eq38 ##| ##39: napply eqop_to_eq39 ##| ##40: napply eqop_to_eq40
 256  ##| ##41: napply eqop_to_eq41 ##| ##42: napply eqop_to_eq42 ##| ##43: napply eqop_to_eq43 ##| ##44: napply eqop_to_eq44
 257  ##| ##45: napply eqop_to_eq45 ##| ##46: napply eqop_to_eq46 ##| ##47: napply eqop_to_eq47 ##| ##48: napply eqop_to_eq48
 258  ##| ##49: napply eqop_to_eq49 ##| ##50: napply eqop_to_eq50 ##| ##51: napply eqop_to_eq51 ##| ##52: napply eqop_to_eq52
 259  ##| ##53: napply eqop_to_eq53 ##| ##54: napply eqop_to_eq54 ##| ##55: napply eqop_to_eq55 ##| ##56: napply eqop_to_eq56
 260  ##| ##57: napply eqop_to_eq57 ##| ##58: napply eqop_to_eq58 ##| ##59: napply eqop_to_eq59 ##| ##60: napply eqop_to_eq60
 261  ##| ##61: napply eqop_to_eq61 ##| ##62: napply eqop_to_eq62 ##| ##63: napply eqop_to_eq63 ##| ##64: napply eqop_to_eq64
 262  ##| ##65: napply eqop_to_eq65 ##| ##66: napply eqop_to_eq66 ##| ##67: napply eqop_to_eq67 ##| ##68: napply eqop_to_eq68
 263  ##| ##69: napply eqop_to_eq69 ##| ##70: napply eqop_to_eq70 ##| ##71: napply eqop_to_eq71 ##| ##72: napply eqop_to_eq72
 264  ##| ##73: napply eqop_to_eq73 ##| ##74: napply eqop_to_eq74 ##| ##75: napply eqop_to_eq75 ##| ##76: napply eqop_to_eq76
 265  ##| ##77: napply eqop_to_eq77 ##| ##78: napply eqop_to_eq78 ##| ##79: napply eqop_to_eq79 ##| ##80: napply eqop_to_eq80
 266  ##| ##81: napply eqop_to_eq81 ##| ##82: napply eqop_to_eq82 ##| ##83: napply eqop_to_eq83 ##| ##84: napply eqop_to_eq84
 267  ##| ##85: napply eqop_to_eq85 ##| ##86: napply eqop_to_eq86 ##| ##87: napply eqop_to_eq87 ##| ##88: napply eqop_to_eq88
 268  ##| ##89: napply eqop_to_eq89 ##| ##90: napply eqop_to_eq90 ##| ##91: napply eqop_to_eq91 ##]
 269 nqed.
 270
 271 nlemma eq_to_eqop1 : ∀op2.ADC = op2 → eq_op ADC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 272 nlemma eq_to_eqop2 : ∀op2.ADD = op2 → eq_op ADD op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 273 nlemma eq_to_eqop3 : ∀op2.AIS = op2 → eq_op AIS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 274 nlemma eq_to_eqop4 : ∀op2.AIX = op2 → eq_op AIX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 275 nlemma eq_to_eqop5 : ∀op2.AND = op2 → eq_op AND op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 276 nlemma eq_to_eqop6 : ∀op2.ASL = op2 → eq_op ASL op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 277 nlemma eq_to_eqop7 : ∀op2.ASR = op2 → eq_op ASR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 278 nlemma eq_to_eqop8 : ∀op2.BCC = op2 → eq_op BCC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 279 nlemma eq_to_eqop9 : ∀op2.BCLRn = op2 → eq_op BCLRn op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 280 nlemma eq_to_eqop10 : ∀op2.BCS = op2 → eq_op BCS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 281 nlemma eq_to_eqop11 : ∀op2.BEQ = op2 → eq_op BEQ op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 282 nlemma eq_to_eqop12 : ∀op2.BGE = op2 → eq_op BGE op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 283 nlemma eq_to_eqop13 : ∀op2.BGND = op2 → eq_op BGND op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 284 nlemma eq_to_eqop14 : ∀op2.BGT = op2 → eq_op BGT op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 285 nlemma eq_to_eqop15 : ∀op2.BHCC = op2 → eq_op BHCC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 286 nlemma eq_to_eqop16 : ∀op2.BHCS = op2 → eq_op BHCS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 287 nlemma eq_to_eqop17 : ∀op2.BHI = op2 → eq_op BHI op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 288 nlemma eq_to_eqop18 : ∀op2.BIH = op2 → eq_op BIH op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 289 nlemma eq_to_eqop19 : ∀op2.BIL = op2 → eq_op BIL op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 290 nlemma eq_to_eqop20 : ∀op2.BIT = op2 → eq_op BIT op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 291 nlemma eq_to_eqop21 : ∀op2.BLE = op2 → eq_op BLE op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 292 nlemma eq_to_eqop22 : ∀op2.BLS = op2 → eq_op BLS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 293 nlemma eq_to_eqop23 : ∀op2.BLT = op2 → eq_op BLT op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 294 nlemma eq_to_eqop24 : ∀op2.BMC = op2 → eq_op BMC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 295 nlemma eq_to_eqop25 : ∀op2.BMI = op2 → eq_op BMI op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 296 nlemma eq_to_eqop26 : ∀op2.BMS = op2 → eq_op BMS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 297 nlemma eq_to_eqop27 : ∀op2.BNE = op2 → eq_op BNE op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 298 nlemma eq_to_eqop28 : ∀op2.BPL = op2 → eq_op BPL op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 299 nlemma eq_to_eqop29 : ∀op2.BRA = op2 → eq_op BRA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 300 nlemma eq_to_eqop30 : ∀op2.BRCLRn = op2 → eq_op BRCLRn op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 301 nlemma eq_to_eqop31 : ∀op2.BRN = op2 → eq_op BRN op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 302 nlemma eq_to_eqop32 : ∀op2.BRSETn = op2 → eq_op BRSETn op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 303 nlemma eq_to_eqop33 : ∀op2.BSETn = op2 → eq_op BSETn op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##33: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 304 nlemma eq_to_eqop34 : ∀op2.BSR = op2 → eq_op BSR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##34: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 305 nlemma eq_to_eqop35 : ∀op2.CBEQA = op2 → eq_op CBEQA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##35: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 306 nlemma eq_to_eqop36 : ∀op2.CBEQX = op2 → eq_op CBEQX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##36: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 307 nlemma eq_to_eqop37 : ∀op2.CLC = op2 → eq_op CLC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##37: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 308 nlemma eq_to_eqop38 : ∀op2.CLI = op2 → eq_op CLI op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##38: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 309 nlemma eq_to_eqop39 : ∀op2.CLR = op2 → eq_op CLR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##39: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 310 nlemma eq_to_eqop40 : ∀op2.CMP = op2 → eq_op CMP op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##40: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 311 nlemma eq_to_eqop41 : ∀op2.COM = op2 → eq_op COM op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##41: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 312 nlemma eq_to_eqop42 : ∀op2.CPHX = op2 → eq_op CPHX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##42: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 313 nlemma eq_to_eqop43 : ∀op2.CPX = op2 → eq_op CPX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##43: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 314 nlemma eq_to_eqop44 : ∀op2.DAA = op2 → eq_op DAA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##44: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 315 nlemma eq_to_eqop45 : ∀op2.DBNZ = op2 → eq_op DBNZ op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##45: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 316 nlemma eq_to_eqop46 : ∀op2.DEC = op2 → eq_op DEC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##46: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 317 nlemma eq_to_eqop47 : ∀op2.DIV = op2 → eq_op DIV op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##47: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 318 nlemma eq_to_eqop48 : ∀op2.EOR = op2 → eq_op EOR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##48: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 319 nlemma eq_to_eqop49 : ∀op2.INC = op2 → eq_op INC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##49: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 320 nlemma eq_to_eqop50 : ∀op2.JMP = op2 → eq_op JMP op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##50: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 321 nlemma eq_to_eqop51 : ∀op2.JSR = op2 → eq_op JSR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##51: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 322 nlemma eq_to_eqop52 : ∀op2.LDA = op2 → eq_op LDA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##52: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 323 nlemma eq_to_eqop53 : ∀op2.LDHX = op2 → eq_op LDHX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##53: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 324 nlemma eq_to_eqop54 : ∀op2.LDX = op2 → eq_op LDX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##54: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 325 nlemma eq_to_eqop55 : ∀op2.LSR = op2 → eq_op LSR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##55: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 326 nlemma eq_to_eqop56 : ∀op2.MOV = op2 → eq_op MOV op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##56: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 327 nlemma eq_to_eqop57 : ∀op2.MUL = op2 → eq_op MUL op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##57: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 328 nlemma eq_to_eqop58 : ∀op2.NEG = op2 → eq_op NEG op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##58: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 329 nlemma eq_to_eqop59 : ∀op2.NOP = op2 → eq_op NOP op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##59: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 330 nlemma eq_to_eqop60 : ∀op2.NSA = op2 → eq_op NSA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##60: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 331 nlemma eq_to_eqop61 : ∀op2.ORA = op2 → eq_op ORA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##61: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 332 nlemma eq_to_eqop62 : ∀op2.PSHA = op2 → eq_op PSHA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##62: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 333 nlemma eq_to_eqop63 : ∀op2.PSHH = op2 → eq_op PSHH op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##63: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 334 nlemma eq_to_eqop64 : ∀op2.PSHX = op2 → eq_op PSHX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##64: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 335 nlemma eq_to_eqop65 : ∀op2.PULA = op2 → eq_op PULA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##65: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 336 nlemma eq_to_eqop66 : ∀op2.PULH = op2 → eq_op PULH op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##66: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 337 nlemma eq_to_eqop67 : ∀op2.PULX = op2 → eq_op PULX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##67: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 338 nlemma eq_to_eqop68 : ∀op2.ROL = op2 → eq_op ROL op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##68: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 339 nlemma eq_to_eqop69 : ∀op2.ROR = op2 → eq_op ROR op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##69: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 340 nlemma eq_to_eqop70 : ∀op2.RSP = op2 → eq_op RSP op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##70: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 341 nlemma eq_to_eqop71 : ∀op2.RTI = op2 → eq_op RTI op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##71: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 342 nlemma eq_to_eqop72 : ∀op2.RTS = op2 → eq_op RTS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##72: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 343 nlemma eq_to_eqop73 : ∀op2.SBC = op2 → eq_op SBC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##73: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 344 nlemma eq_to_eqop74 : ∀op2.SEC = op2 → eq_op SEC op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##74: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 345 nlemma eq_to_eqop75 : ∀op2.SEI = op2 → eq_op SEI op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##75: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 346 nlemma eq_to_eqop76 : ∀op2.SHA = op2 → eq_op SHA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##76: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 347 nlemma eq_to_eqop77 : ∀op2.SLA = op2 → eq_op SLA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##77: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 348 nlemma eq_to_eqop78 : ∀op2.STA = op2 → eq_op STA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##78: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 349 nlemma eq_to_eqop79 : ∀op2.STHX = op2 → eq_op STHX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##79: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 350 nlemma eq_to_eqop80 : ∀op2.STOP = op2 → eq_op STOP op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##80: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 351 nlemma eq_to_eqop81 : ∀op2.STX = op2 → eq_op STX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##81: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 352 nlemma eq_to_eqop82 : ∀op2.SUB = op2 → eq_op SUB op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##82: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 353 nlemma eq_to_eqop83 : ∀op2.SWI = op2 → eq_op SWI op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##83: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 354 nlemma eq_to_eqop84 : ∀op2.TAP = op2 → eq_op TAP op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##84: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 355 nlemma eq_to_eqop85 : ∀op2.TAX = op2 → eq_op TAX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##85: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 356 nlemma eq_to_eqop86 : ∀op2.TPA = op2 → eq_op TPA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##86: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 357 nlemma eq_to_eqop87 : ∀op2.TST = op2 → eq_op TST op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##87: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 358 nlemma eq_to_eqop88 : ∀op2.TSX = op2 → eq_op TSX op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##88: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 359 nlemma eq_to_eqop89 : ∀op2.TXA = op2 → eq_op TXA op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##89: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 360 nlemma eq_to_eqop90 : ∀op2.TXS = op2 → eq_op TXS op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##90: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 361 nlemma eq_to_eqop91 : ∀op2.WAIT = op2 → eq_op WAIT op2 = true. #op2; ncases op2; nnormalize; #H; ##[ ##91: napply (refl_eq ??) ##| ##*: napply (opcode_destruct ?? (false = true) H) ##]nqed.
 362
 363 nlemma eq_to_eqop : ∀op1,op2.op1 = op2 → eq_op op1 op2 = true.
 364  #op1; ncases op1;
 365  ##[ ##1: napply eq_to_eqop1 ##| ##2: napply eq_to_eqop2 ##| ##3: napply eq_to_eqop3 ##| ##4: napply eq_to_eqop4
 366  ##| ##5: napply eq_to_eqop5 ##| ##6: napply eq_to_eqop6 ##| ##7: napply eq_to_eqop7 ##| ##8: napply eq_to_eqop8
 367  ##| ##9: napply eq_to_eqop9 ##| ##10: napply eq_to_eqop10 ##| ##11: napply eq_to_eqop11 ##| ##12: napply eq_to_eqop12
 368  ##| ##13: napply eq_to_eqop13 ##| ##14: napply eq_to_eqop14 ##| ##15: napply eq_to_eqop15 ##| ##16: napply eq_to_eqop16
 369  ##| ##17: napply eq_to_eqop17 ##| ##18: napply eq_to_eqop18 ##| ##19: napply eq_to_eqop19 ##| ##20: napply eq_to_eqop20
 370  ##| ##21: napply eq_to_eqop21 ##| ##22: napply eq_to_eqop22 ##| ##23: napply eq_to_eqop23 ##| ##24: napply eq_to_eqop24
 371  ##| ##25: napply eq_to_eqop25 ##| ##26: napply eq_to_eqop26 ##| ##27: napply eq_to_eqop27 ##| ##28: napply eq_to_eqop28
 372  ##| ##29: napply eq_to_eqop29 ##| ##30: napply eq_to_eqop30 ##| ##31: napply eq_to_eqop31 ##| ##32: napply eq_to_eqop32
 373  ##| ##33: napply eq_to_eqop33 ##| ##34: napply eq_to_eqop34 ##| ##35: napply eq_to_eqop35 ##| ##36: napply eq_to_eqop36
 374  ##| ##37: napply eq_to_eqop37 ##| ##38: napply eq_to_eqop38 ##| ##39: napply eq_to_eqop39 ##| ##40: napply eq_to_eqop40
 375  ##| ##41: napply eq_to_eqop41 ##| ##42: napply eq_to_eqop42 ##| ##43: napply eq_to_eqop43 ##| ##44: napply eq_to_eqop44
 376  ##| ##45: napply eq_to_eqop45 ##| ##46: napply eq_to_eqop46 ##| ##47: napply eq_to_eqop47 ##| ##48: napply eq_to_eqop48
 377  ##| ##49: napply eq_to_eqop49 ##| ##50: napply eq_to_eqop50 ##| ##51: napply eq_to_eqop51 ##| ##52: napply eq_to_eqop52
 378  ##| ##53: napply eq_to_eqop53 ##| ##54: napply eq_to_eqop54 ##| ##55: napply eq_to_eqop55 ##| ##56: napply eq_to_eqop56
 379  ##| ##57: napply eq_to_eqop57 ##| ##58: napply eq_to_eqop58 ##| ##59: napply eq_to_eqop59 ##| ##60: napply eq_to_eqop60
 380  ##| ##61: napply eq_to_eqop61 ##| ##62: napply eq_to_eqop62 ##| ##63: napply eq_to_eqop63 ##| ##64: napply eq_to_eqop64
 381  ##| ##65: napply eq_to_eqop65 ##| ##66: napply eq_to_eqop66 ##| ##67: napply eq_to_eqop67 ##| ##68: napply eq_to_eqop68
 382  ##| ##69: napply eq_to_eqop69 ##| ##70: napply eq_to_eqop70 ##| ##71: napply eq_to_eqop71 ##| ##72: napply eq_to_eqop72
 383  ##| ##73: napply eq_to_eqop73 ##| ##74: napply eq_to_eqop74 ##| ##75: napply eq_to_eqop75 ##| ##76: napply eq_to_eqop76
 384  ##| ##77: napply eq_to_eqop77 ##| ##78: napply eq_to_eqop78 ##| ##79: napply eq_to_eqop79 ##| ##80: napply eq_to_eqop80
 385  ##| ##81: napply eq_to_eqop81 ##| ##82: napply eq_to_eqop82 ##| ##83: napply eq_to_eqop83 ##| ##84: napply eq_to_eqop84
 386  ##| ##85: napply eq_to_eqop85 ##| ##86: napply eq_to_eqop86 ##| ##87: napply eq_to_eqop87 ##| ##88: napply eq_to_eqop88
 387  ##| ##89: napply eq_to_eqop89 ##| ##90: napply eq_to_eqop90 ##| ##91: napply eq_to_eqop91 ##]
 388 nqed.