freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode_base_lemmas_opcode2.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma
index a14cd58019a4900af4948bed160aca3c6e9a6ba7..dca4a5d5720d9bf7e6dcb10021c219d3645bc3a7 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_opcode2.ma
@@ -26,359 +26,359 @@ include "freescale/opcode_base_lemmas_opcode1.ma".
 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
 (* ********************************************** *)
 
-nlemma symmetric_eqop1 : ∀op2.eq_op ADC op2 = eq_op op2 ADC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop2 : ∀op2.eq_op ADD op2 = eq_op op2 ADD. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop3 : ∀op2.eq_op AIS op2 = eq_op op2 AIS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop4 : ∀op2.eq_op AIX op2 = eq_op op2 AIX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop5 : ∀op2.eq_op AND op2 = eq_op op2 AND. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop6 : ∀op2.eq_op ASL op2 = eq_op op2 ASL. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop7 : ∀op2.eq_op ASR op2 = eq_op op2 ASR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop8 : ∀op2.eq_op BCC op2 = eq_op op2 BCC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop9 : ∀op2.eq_op BCLRn op2 = eq_op op2 BCLRn. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop10 : ∀op2.eq_op BCS op2 = eq_op op2 BCS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop11 : ∀op2.eq_op BEQ op2 = eq_op op2 BEQ. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop12 : ∀op2.eq_op BGE op2 = eq_op op2 BGE. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop13 : ∀op2.eq_op BGND op2 = eq_op op2 BGND. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop14 : ∀op2.eq_op BGT op2 = eq_op op2 BGT. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop15 : ∀op2.eq_op BHCC op2 = eq_op op2 BHCC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop16 : ∀op2.eq_op BHCS op2 = eq_op op2 BHCS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop17 : ∀op2.eq_op BHI op2 = eq_op op2 BHI. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop18 : ∀op2.eq_op BIH op2 = eq_op op2 BIH. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop19 : ∀op2.eq_op BIL op2 = eq_op op2 BIL. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop20 : ∀op2.eq_op BIT op2 = eq_op op2 BIT. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop21 : ∀op2.eq_op BLE op2 = eq_op op2 BLE. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop22 : ∀op2.eq_op BLS op2 = eq_op op2 BLS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop23 : ∀op2.eq_op BLT op2 = eq_op op2 BLT. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop24 : ∀op2.eq_op BMC op2 = eq_op op2 BMC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop25 : ∀op2.eq_op BMI op2 = eq_op op2 BMI. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop26 : ∀op2.eq_op BMS op2 = eq_op op2 BMS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop27 : ∀op2.eq_op BNE op2 = eq_op op2 BNE. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop28 : ∀op2.eq_op BPL op2 = eq_op op2 BPL. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop29 : ∀op2.eq_op BRA op2 = eq_op op2 BRA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop30 : ∀op2.eq_op BRCLRn op2 = eq_op op2 BRCLRn. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop31 : ∀op2.eq_op BRN op2 = eq_op op2 BRN. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop32 : ∀op2.eq_op BRSETn op2 = eq_op op2 BRSETn. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop33 : ∀op2.eq_op BSETn op2 = eq_op op2 BSETn. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop34 : ∀op2.eq_op BSR op2 = eq_op op2 BSR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop35 : ∀op2.eq_op CBEQA op2 = eq_op op2 CBEQA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop36 : ∀op2.eq_op CBEQX op2 = eq_op op2 CBEQX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop37 : ∀op2.eq_op CLC op2 = eq_op op2 CLC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop38 : ∀op2.eq_op CLI op2 = eq_op op2 CLI. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop39 : ∀op2.eq_op CLR op2 = eq_op op2 CLR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop40 : ∀op2.eq_op CMP op2 = eq_op op2 CMP. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop41 : ∀op2.eq_op COM op2 = eq_op op2 COM. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop42 : ∀op2.eq_op CPHX op2 = eq_op op2 CPHX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop43 : ∀op2.eq_op CPX op2 = eq_op op2 CPX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop44 : ∀op2.eq_op DAA op2 = eq_op op2 DAA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop45 : ∀op2.eq_op DBNZ op2 = eq_op op2 DBNZ. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop46 : ∀op2.eq_op DEC op2 = eq_op op2 DEC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop47 : ∀op2.eq_op DIV op2 = eq_op op2 DIV. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop48 : ∀op2.eq_op EOR op2 = eq_op op2 EOR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop49 : ∀op2.eq_op INC op2 = eq_op op2 INC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop50 : ∀op2.eq_op JMP op2 = eq_op op2 JMP. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop51 : ∀op2.eq_op JSR op2 = eq_op op2 JSR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop52 : ∀op2.eq_op LDA op2 = eq_op op2 LDA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop53 : ∀op2.eq_op LDHX op2 = eq_op op2 LDHX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop54 : ∀op2.eq_op LDX op2 = eq_op op2 LDX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop55 : ∀op2.eq_op LSR op2 = eq_op op2 LSR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop56 : ∀op2.eq_op MOV op2 = eq_op op2 MOV. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop57 : ∀op2.eq_op MUL op2 = eq_op op2 MUL. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop58 : ∀op2.eq_op NEG op2 = eq_op op2 NEG. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop59 : ∀op2.eq_op NOP op2 = eq_op op2 NOP. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop60 : ∀op2.eq_op NSA op2 = eq_op op2 NSA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop61 : ∀op2.eq_op ORA op2 = eq_op op2 ORA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop62 : ∀op2.eq_op PSHA op2 = eq_op op2 PSHA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop63 : ∀op2.eq_op PSHH op2 = eq_op op2 PSHH. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop64 : ∀op2.eq_op PSHX op2 = eq_op op2 PSHX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop65 : ∀op2.eq_op PULA op2 = eq_op op2 PULA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop66 : ∀op2.eq_op PULH op2 = eq_op op2 PULH. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop67 : ∀op2.eq_op PULX op2 = eq_op op2 PULX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop68 : ∀op2.eq_op ROL op2 = eq_op op2 ROL. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop69 : ∀op2.eq_op ROR op2 = eq_op op2 ROR. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop70 : ∀op2.eq_op RSP op2 = eq_op op2 RSP. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop71 : ∀op2.eq_op RTI op2 = eq_op op2 RTI. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop72 : ∀op2.eq_op RTS op2 = eq_op op2 RTS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop73 : ∀op2.eq_op SBC op2 = eq_op op2 SBC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop74 : ∀op2.eq_op SEC op2 = eq_op op2 SEC. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop75 : ∀op2.eq_op SEI op2 = eq_op op2 SEI. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop76 : ∀op2.eq_op SHA op2 = eq_op op2 SHA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop77 : ∀op2.eq_op SLA op2 = eq_op op2 SLA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop78 : ∀op2.eq_op STA op2 = eq_op op2 STA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop79 : ∀op2.eq_op STHX op2 = eq_op op2 STHX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop80 : ∀op2.eq_op STOP op2 = eq_op op2 STOP. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop81 : ∀op2.eq_op STX op2 = eq_op op2 STX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop82 : ∀op2.eq_op SUB op2 = eq_op op2 SUB. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop83 : ∀op2.eq_op SWI op2 = eq_op op2 SWI. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop84 : ∀op2.eq_op TAP op2 = eq_op op2 TAP. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop85 : ∀op2.eq_op TAX op2 = eq_op op2 TAX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop86 : ∀op2.eq_op TPA op2 = eq_op op2 TPA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop87 : ∀op2.eq_op TST op2 = eq_op op2 TST. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop88 : ∀op2.eq_op TSX op2 = eq_op op2 TSX. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop89 : ∀op2.eq_op TXA op2 = eq_op op2 TXA. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop90 : ∀op2.eq_op TXS op2 = eq_op op2 TXS. #op2; nnormalize; napply refl_eq.nqed.
-nlemma symmetric_eqop91 : ∀op2.eq_op WAIT op2 = eq_op op2 WAIT. #op2; nnormalize; napply refl_eq.nqed.
+nlemma decidable_op1 : ∀x:opcode.decidable (ADC = x). #x; nnormalize; nelim x; ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op2 : ∀x:opcode.decidable (ADD = x). #x; nnormalize; nelim x; ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op3 : ∀x:opcode.decidable (AIS = x). #x; nnormalize; nelim x; ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op4 : ∀x:opcode.decidable (AIX = x). #x; nnormalize; nelim x; ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op5 : ∀x:opcode.decidable (AND = x). #x; nnormalize; nelim x; ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op6 : ∀x:opcode.decidable (ASL = x). #x; nnormalize; nelim x; ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op7 : ∀x:opcode.decidable (ASR = x). #x; nnormalize; nelim x; ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op8 : ∀x:opcode.decidable (BCC = x). #x; nnormalize; nelim x; ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op9 : ∀x:opcode.decidable (BCLRn = x). #x; nnormalize; nelim x; ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op10 : ∀x:opcode.decidable (BCS = x). #x; nnormalize; nelim x; ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op11 : ∀x:opcode.decidable (BEQ = x). #x; nnormalize; nelim x; ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op12 : ∀x:opcode.decidable (BGE = x). #x; nnormalize; nelim x; ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op13 : ∀x:opcode.decidable (BGND = x). #x; nnormalize; nelim x; ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op14 : ∀x:opcode.decidable (BGT = x). #x; nnormalize; nelim x; ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op15 : ∀x:opcode.decidable (BHCC = x). #x; nnormalize; nelim x; ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op16 : ∀x:opcode.decidable (BHCS = x). #x; nnormalize; nelim x; ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op17 : ∀x:opcode.decidable (BHI = x). #x; nnormalize; nelim x; ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op18 : ∀x:opcode.decidable (BIH = x). #x; nnormalize; nelim x; ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op19 : ∀x:opcode.decidable (BIL = x). #x; nnormalize; nelim x; ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op20 : ∀x:opcode.decidable (BIT = x). #x; nnormalize; nelim x; ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op21 : ∀x:opcode.decidable (BLE = x). #x; nnormalize; nelim x; ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op22 : ∀x:opcode.decidable (BLS = x). #x; nnormalize; nelim x; ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op23 : ∀x:opcode.decidable (BLT = x). #x; nnormalize; nelim x; ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op24 : ∀x:opcode.decidable (BMC = x). #x; nnormalize; nelim x; ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op25 : ∀x:opcode.decidable (BMI = x). #x; nnormalize; nelim x; ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op26 : ∀x:opcode.decidable (BMS = x). #x; nnormalize; nelim x; ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op27 : ∀x:opcode.decidable (BNE = x). #x; nnormalize; nelim x; ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op28 : ∀x:opcode.decidable (BPL = x). #x; nnormalize; nelim x; ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op29 : ∀x:opcode.decidable (BRA = x). #x; nnormalize; nelim x; ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op30 : ∀x:opcode.decidable (BRCLRn = x). #x; nnormalize; nelim x; ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op31 : ∀x:opcode.decidable (BRN = x). #x; nnormalize; nelim x; ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op32 : ∀x:opcode.decidable (BRSETn = x). #x; nnormalize; nelim x; ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op33 : ∀x:opcode.decidable (BSETn = x). #x; nnormalize; nelim x; ##[ ##33: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op34 : ∀x:opcode.decidable (BSR = x). #x; nnormalize; nelim x; ##[ ##34: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op35 : ∀x:opcode.decidable (CBEQA = x). #x; nnormalize; nelim x; ##[ ##35: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op36 : ∀x:opcode.decidable (CBEQX = x). #x; nnormalize; nelim x; ##[ ##36: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op37 : ∀x:opcode.decidable (CLC = x). #x; nnormalize; nelim x; ##[ ##37: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op38 : ∀x:opcode.decidable (CLI = x). #x; nnormalize; nelim x; ##[ ##38: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op39 : ∀x:opcode.decidable (CLR = x). #x; nnormalize; nelim x; ##[ ##39: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op40 : ∀x:opcode.decidable (CMP = x). #x; nnormalize; nelim x; ##[ ##40: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op41 : ∀x:opcode.decidable (COM = x). #x; nnormalize; nelim x; ##[ ##41: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op42 : ∀x:opcode.decidable (CPHX = x). #x; nnormalize; nelim x; ##[ ##42: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op43 : ∀x:opcode.decidable (CPX = x). #x; nnormalize; nelim x; ##[ ##43: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op44 : ∀x:opcode.decidable (DAA = x). #x; nnormalize; nelim x; ##[ ##44: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op45 : ∀x:opcode.decidable (DBNZ = x). #x; nnormalize; nelim x; ##[ ##45: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op46 : ∀x:opcode.decidable (DEC = x). #x; nnormalize; nelim x; ##[ ##46: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op47 : ∀x:opcode.decidable (DIV = x). #x; nnormalize; nelim x; ##[ ##47: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op48 : ∀x:opcode.decidable (EOR = x). #x; nnormalize; nelim x; ##[ ##48: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op49 : ∀x:opcode.decidable (INC = x). #x; nnormalize; nelim x; ##[ ##49: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op50 : ∀x:opcode.decidable (JMP = x). #x; nnormalize; nelim x; ##[ ##50: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op51 : ∀x:opcode.decidable (JSR = x). #x; nnormalize; nelim x; ##[ ##51: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op52 : ∀x:opcode.decidable (LDA = x). #x; nnormalize; nelim x; ##[ ##52: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op53 : ∀x:opcode.decidable (LDHX = x). #x; nnormalize; nelim x; ##[ ##53: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op54 : ∀x:opcode.decidable (LDX = x). #x; nnormalize; nelim x; ##[ ##54: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op55 : ∀x:opcode.decidable (LSR = x). #x; nnormalize; nelim x; ##[ ##55: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op56 : ∀x:opcode.decidable (MOV = x). #x; nnormalize; nelim x; ##[ ##56: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op57 : ∀x:opcode.decidable (MUL = x). #x; nnormalize; nelim x; ##[ ##57: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op58 : ∀x:opcode.decidable (NEG = x). #x; nnormalize; nelim x; ##[ ##58: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op59 : ∀x:opcode.decidable (NOP = x). #x; nnormalize; nelim x; ##[ ##59: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op60 : ∀x:opcode.decidable (NSA = x). #x; nnormalize; nelim x; ##[ ##60: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op61 : ∀x:opcode.decidable (ORA = x). #x; nnormalize; nelim x; ##[ ##61: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op62 : ∀x:opcode.decidable (PSHA = x). #x; nnormalize; nelim x; ##[ ##62: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op63 : ∀x:opcode.decidable (PSHH = x). #x; nnormalize; nelim x; ##[ ##63: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op64 : ∀x:opcode.decidable (PSHX = x). #x; nnormalize; nelim x; ##[ ##64: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op65 : ∀x:opcode.decidable (PULA = x). #x; nnormalize; nelim x; ##[ ##65: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op66 : ∀x:opcode.decidable (PULH = x). #x; nnormalize; nelim x; ##[ ##66: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op67 : ∀x:opcode.decidable (PULX = x). #x; nnormalize; nelim x; ##[ ##67: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op68 : ∀x:opcode.decidable (ROL = x). #x; nnormalize; nelim x; ##[ ##68: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op69 : ∀x:opcode.decidable (ROR = x). #x; nnormalize; nelim x; ##[ ##69: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op70 : ∀x:opcode.decidable (RSP = x). #x; nnormalize; nelim x; ##[ ##70: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op71 : ∀x:opcode.decidable (RTI = x). #x; nnormalize; nelim x; ##[ ##71: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op72 : ∀x:opcode.decidable (RTS = x). #x; nnormalize; nelim x; ##[ ##72: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op73 : ∀x:opcode.decidable (SBC = x). #x; nnormalize; nelim x; ##[ ##73: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op74 : ∀x:opcode.decidable (SEC = x). #x; nnormalize; nelim x; ##[ ##74: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op75 : ∀x:opcode.decidable (SEI = x). #x; nnormalize; nelim x; ##[ ##75: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op76 : ∀x:opcode.decidable (SHA = x). #x; nnormalize; nelim x; ##[ ##76: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op77 : ∀x:opcode.decidable (SLA = x). #x; nnormalize; nelim x; ##[ ##77: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op78 : ∀x:opcode.decidable (STA = x). #x; nnormalize; nelim x; ##[ ##78: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op79 : ∀x:opcode.decidable (STHX = x). #x; nnormalize; nelim x; ##[ ##79: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op80 : ∀x:opcode.decidable (STOP = x). #x; nnormalize; nelim x; ##[ ##80: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op81 : ∀x:opcode.decidable (STX = x). #x; nnormalize; nelim x; ##[ ##81: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op82 : ∀x:opcode.decidable (SUB = x). #x; nnormalize; nelim x; ##[ ##82: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op83 : ∀x:opcode.decidable (SWI = x). #x; nnormalize; nelim x; ##[ ##83: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op84 : ∀x:opcode.decidable (TAP = x). #x; nnormalize; nelim x; ##[ ##84: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op85 : ∀x:opcode.decidable (TAX = x). #x; nnormalize; nelim x; ##[ ##85: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op86 : ∀x:opcode.decidable (TPA = x). #x; nnormalize; nelim x; ##[ ##86: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op87 : ∀x:opcode.decidable (TST = x). #x; nnormalize; nelim x; ##[ ##87: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op88 : ∀x:opcode.decidable (TSX = x). #x; nnormalize; nelim x; ##[ ##88: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op89 : ∀x:opcode.decidable (TXA = x). #x; nnormalize; nelim x; ##[ ##89: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op90 : ∀x:opcode.decidable (TXS = x). #x; nnormalize; nelim x; ##[ ##90: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
+nlemma decidable_op91 : ∀x:opcode.decidable (WAIT = x). #x; nnormalize; nelim x; ##[ ##91: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (opcode_destruct … H) ##] nqed.
 
-nlemma symmetric_eqop : symmetricT opcode bool eq_op.
+nlemma decidable_op : ∀x,y:opcode.decidable (x = y).
  #op1; ncases op1;
- ##[ ##1: napply symmetric_eqop1 ##| ##2: napply symmetric_eqop2 ##| ##3: napply symmetric_eqop3 ##| ##4: napply symmetric_eqop4
- ##| ##5: napply symmetric_eqop5 ##| ##6: napply symmetric_eqop6 ##| ##7: napply symmetric_eqop7 ##| ##8: napply symmetric_eqop8
- ##| ##9: napply symmetric_eqop9 ##| ##10: napply symmetric_eqop10 ##| ##11: napply symmetric_eqop11 ##| ##12: napply symmetric_eqop12
- ##| ##13: napply symmetric_eqop13 ##| ##14: napply symmetric_eqop14 ##| ##15: napply symmetric_eqop15 ##| ##16: napply symmetric_eqop16
- ##| ##17: napply symmetric_eqop17 ##| ##18: napply symmetric_eqop18 ##| ##19: napply symmetric_eqop19 ##| ##20: napply symmetric_eqop20
- ##| ##21: napply symmetric_eqop21 ##| ##22: napply symmetric_eqop22 ##| ##23: napply symmetric_eqop23 ##| ##24: napply symmetric_eqop24
- ##| ##25: napply symmetric_eqop25 ##| ##26: napply symmetric_eqop26 ##| ##27: napply symmetric_eqop27 ##| ##28: napply symmetric_eqop28
- ##| ##29: napply symmetric_eqop29 ##| ##30: napply symmetric_eqop30 ##| ##31: napply symmetric_eqop31 ##| ##32: napply symmetric_eqop32
- ##| ##33: napply symmetric_eqop33 ##| ##34: napply symmetric_eqop34 ##| ##35: napply symmetric_eqop35 ##| ##36: napply symmetric_eqop36
- ##| ##37: napply symmetric_eqop37 ##| ##38: napply symmetric_eqop38 ##| ##39: napply symmetric_eqop39 ##| ##40: napply symmetric_eqop40
- ##| ##41: napply symmetric_eqop41 ##| ##42: napply symmetric_eqop42 ##| ##43: napply symmetric_eqop43 ##| ##44: napply symmetric_eqop44
- ##| ##45: napply symmetric_eqop45 ##| ##46: napply symmetric_eqop46 ##| ##47: napply symmetric_eqop47 ##| ##48: napply symmetric_eqop48
- ##| ##49: napply symmetric_eqop49 ##| ##50: napply symmetric_eqop50 ##| ##51: napply symmetric_eqop51 ##| ##52: napply symmetric_eqop52
- ##| ##53: napply symmetric_eqop53 ##| ##54: napply symmetric_eqop54 ##| ##55: napply symmetric_eqop55 ##| ##56: napply symmetric_eqop56
- ##| ##57: napply symmetric_eqop57 ##| ##58: napply symmetric_eqop58 ##| ##59: napply symmetric_eqop59 ##| ##60: napply symmetric_eqop60
- ##| ##61: napply symmetric_eqop61 ##| ##62: napply symmetric_eqop62 ##| ##63: napply symmetric_eqop63 ##| ##64: napply symmetric_eqop64
- ##| ##65: napply symmetric_eqop65 ##| ##66: napply symmetric_eqop66 ##| ##67: napply symmetric_eqop67 ##| ##68: napply symmetric_eqop68
- ##| ##69: napply symmetric_eqop69 ##| ##70: napply symmetric_eqop70 ##| ##71: napply symmetric_eqop71 ##| ##72: napply symmetric_eqop72
- ##| ##73: napply symmetric_eqop73 ##| ##74: napply symmetric_eqop74 ##| ##75: napply symmetric_eqop75 ##| ##76: napply symmetric_eqop76
- ##| ##77: napply symmetric_eqop77 ##| ##78: napply symmetric_eqop78 ##| ##79: napply symmetric_eqop79 ##| ##80: napply symmetric_eqop80
- ##| ##81: napply symmetric_eqop81 ##| ##82: napply symmetric_eqop82 ##| ##83: napply symmetric_eqop83 ##| ##84: napply symmetric_eqop84
- ##| ##85: napply symmetric_eqop85 ##| ##86: napply symmetric_eqop86 ##| ##87: napply symmetric_eqop87 ##| ##88: napply symmetric_eqop88
- ##| ##89: napply symmetric_eqop89 ##| ##90: napply symmetric_eqop90 ##| ##91: napply symmetric_eqop91 ##]
+ ##[ ##1: napply decidable_op1 ##| ##2: napply decidable_op2 ##| ##3: napply decidable_op3 ##| ##4: napply decidable_op4
+ ##| ##5: napply decidable_op5 ##| ##6: napply decidable_op6 ##| ##7: napply decidable_op7 ##| ##8: napply decidable_op8
+ ##| ##9: napply decidable_op9 ##| ##10: napply decidable_op10 ##| ##11: napply decidable_op11 ##| ##12: napply decidable_op12
+ ##| ##13: napply decidable_op13 ##| ##14: napply decidable_op14 ##| ##15: napply decidable_op15 ##| ##16: napply decidable_op16
+ ##| ##17: napply decidable_op17 ##| ##18: napply decidable_op18 ##| ##19: napply decidable_op19 ##| ##20: napply decidable_op20
+ ##| ##21: napply decidable_op21 ##| ##22: napply decidable_op22 ##| ##23: napply decidable_op23 ##| ##24: napply decidable_op24
+ ##| ##25: napply decidable_op25 ##| ##26: napply decidable_op26 ##| ##27: napply decidable_op27 ##| ##28: napply decidable_op28
+ ##| ##29: napply decidable_op29 ##| ##30: napply decidable_op30 ##| ##31: napply decidable_op31 ##| ##32: napply decidable_op32
+ ##| ##33: napply decidable_op33 ##| ##34: napply decidable_op34 ##| ##35: napply decidable_op35 ##| ##36: napply decidable_op36
+ ##| ##37: napply decidable_op37 ##| ##38: napply decidable_op38 ##| ##39: napply decidable_op39 ##| ##40: napply decidable_op40
+ ##| ##41: napply decidable_op41 ##| ##42: napply decidable_op42 ##| ##43: napply decidable_op43 ##| ##44: napply decidable_op44
+ ##| ##45: napply decidable_op45 ##| ##46: napply decidable_op46 ##| ##47: napply decidable_op47 ##| ##48: napply decidable_op48
+ ##| ##49: napply decidable_op49 ##| ##50: napply decidable_op50 ##| ##51: napply decidable_op51 ##| ##52: napply decidable_op52
+ ##| ##53: napply decidable_op53 ##| ##54: napply decidable_op54 ##| ##55: napply decidable_op55 ##| ##56: napply decidable_op56
+ ##| ##57: napply decidable_op57 ##| ##58: napply decidable_op58 ##| ##59: napply decidable_op59 ##| ##60: napply decidable_op60
+ ##| ##61: napply decidable_op61 ##| ##62: napply decidable_op62 ##| ##63: napply decidable_op63 ##| ##64: napply decidable_op64
+ ##| ##65: napply decidable_op65 ##| ##66: napply decidable_op66 ##| ##67: napply decidable_op67 ##| ##68: napply decidable_op68
+ ##| ##69: napply decidable_op69 ##| ##70: napply decidable_op70 ##| ##71: napply decidable_op71 ##| ##72: napply decidable_op72
+ ##| ##73: napply decidable_op73 ##| ##74: napply decidable_op74 ##| ##75: napply decidable_op75 ##| ##76: napply decidable_op76
+ ##| ##77: napply decidable_op77 ##| ##78: napply decidable_op78 ##| ##79: napply decidable_op79 ##| ##80: napply decidable_op80
+ ##| ##81: napply decidable_op81 ##| ##82: napply decidable_op82 ##| ##83: napply decidable_op83 ##| ##84: napply decidable_op84
+ ##| ##85: napply decidable_op85 ##| ##86: napply decidable_op86 ##| ##87: napply decidable_op87 ##| ##88: napply decidable_op88
+ ##| ##89: napply decidable_op89 ##| ##90: napply decidable_op90 ##| ##91: napply decidable_op91 ##]
 nqed.
 
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
+nlemma neqop_to_neq1 : ∀op2.eq_op ADC op2 = false → ADC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##1: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq2 : ∀op2.eq_op ADD op2 = false → ADD ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##2: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq3 : ∀op2.eq_op AIS op2 = false → AIS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##3: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq4 : ∀op2.eq_op AIX op2 = false → AIX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##4: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq5 : ∀op2.eq_op AND op2 = false → AND ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##5: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq6 : ∀op2.eq_op ASL op2 = false → ASL ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##6: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq7 : ∀op2.eq_op ASR op2 = false → ASR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##7: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq8 : ∀op2.eq_op BCC op2 = false → BCC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##8: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq9 : ∀op2.eq_op BCLRn op2 = false → BCLRn ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##9: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq10 : ∀op2.eq_op BCS op2 = false → BCS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##10: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq11 : ∀op2.eq_op BEQ op2 = false → BEQ ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##11: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq12 : ∀op2.eq_op BGE op2 = false → BGE ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##12: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq13 : ∀op2.eq_op BGND op2 = false → BGND ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##13: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq14 : ∀op2.eq_op BGT op2 = false → BGT ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##14: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq15 : ∀op2.eq_op BHCC op2 = false → BHCC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##15: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq16 : ∀op2.eq_op BHCS op2 = false → BHCS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##16: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq17 : ∀op2.eq_op BHI op2 = false → BHI ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##17: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq18 : ∀op2.eq_op BIH op2 = false → BIH ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##18: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq19 : ∀op2.eq_op BIL op2 = false → BIL ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##19: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq20 : ∀op2.eq_op BIT op2 = false → BIT ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##20: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq21 : ∀op2.eq_op BLE op2 = false → BLE ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##21: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq22 : ∀op2.eq_op BLS op2 = false → BLS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##22: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq23 : ∀op2.eq_op BLT op2 = false → BLT ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##23: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq24 : ∀op2.eq_op BMC op2 = false → BMC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##24: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq25 : ∀op2.eq_op BMI op2 = false → BMI ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##25: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq26 : ∀op2.eq_op BMS op2 = false → BMS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##26: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq27 : ∀op2.eq_op BNE op2 = false → BNE ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##27: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq28 : ∀op2.eq_op BPL op2 = false → BPL ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##28: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq29 : ∀op2.eq_op BRA op2 = false → BRA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##29: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq30 : ∀op2.eq_op BRCLRn op2 = false → BRCLRn ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##30: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq31 : ∀op2.eq_op BRN op2 = false → BRN ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##31: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq32 : ∀op2.eq_op BRSETn op2 = false → BRSETn ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##32: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq33 : ∀op2.eq_op BSETn op2 = false → BSETn ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##33: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq34 : ∀op2.eq_op BSR op2 = false → BSR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##34: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq35 : ∀op2.eq_op CBEQA op2 = false → CBEQA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##35: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq36 : ∀op2.eq_op CBEQX op2 = false → CBEQX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##36: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq37 : ∀op2.eq_op CLC op2 = false → CLC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##37: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq38 : ∀op2.eq_op CLI op2 = false → CLI ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##38: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq39 : ∀op2.eq_op CLR op2 = false → CLR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##39: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq40 : ∀op2.eq_op CMP op2 = false → CMP ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##40: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq41 : ∀op2.eq_op COM op2 = false → COM ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##41: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq42 : ∀op2.eq_op CPHX op2 = false → CPHX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##42: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq43 : ∀op2.eq_op CPX op2 = false → CPX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##43: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq44 : ∀op2.eq_op DAA op2 = false → DAA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##44: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq45 : ∀op2.eq_op DBNZ op2 = false → DBNZ ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##45: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq46 : ∀op2.eq_op DEC op2 = false → DEC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##46: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq47 : ∀op2.eq_op DIV op2 = false → DIV ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##47: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq48 : ∀op2.eq_op EOR op2 = false → EOR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##48: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq49 : ∀op2.eq_op INC op2 = false → INC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##49: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq50 : ∀op2.eq_op JMP op2 = false → JMP ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##50: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq51 : ∀op2.eq_op JSR op2 = false → JSR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##51: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq52 : ∀op2.eq_op LDA op2 = false → LDA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##52: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq53 : ∀op2.eq_op LDHX op2 = false → LDHX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##53: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq54 : ∀op2.eq_op LDX op2 = false → LDX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##54: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq55 : ∀op2.eq_op LSR op2 = false → LSR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##55: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq56 : ∀op2.eq_op MOV op2 = false → MOV ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##56: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq57 : ∀op2.eq_op MUL op2 = false → MUL ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##57: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq58 : ∀op2.eq_op NEG op2 = false → NEG ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##58: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq59 : ∀op2.eq_op NOP op2 = false → NOP ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##59: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq60 : ∀op2.eq_op NSA op2 = false → NSA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##60: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq61 : ∀op2.eq_op ORA op2 = false → ORA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##61: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq62 : ∀op2.eq_op PSHA op2 = false → PSHA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##62: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq63 : ∀op2.eq_op PSHH op2 = false → PSHH ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##63: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq64 : ∀op2.eq_op PSHX op2 = false → PSHX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##64: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq65 : ∀op2.eq_op PULA op2 = false → PULA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##65: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq66 : ∀op2.eq_op PULH op2 = false → PULH ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##66: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq67 : ∀op2.eq_op PULX op2 = false → PULX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##67: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq68 : ∀op2.eq_op ROL op2 = false → ROL ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##68: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq69 : ∀op2.eq_op ROR op2 = false → ROR ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##69: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq70 : ∀op2.eq_op RSP op2 = false → RSP ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##70: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq71 : ∀op2.eq_op RTI op2 = false → RTI ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##71: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq72 : ∀op2.eq_op RTS op2 = false → RTS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##72: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq73 : ∀op2.eq_op SBC op2 = false → SBC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##73: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq74 : ∀op2.eq_op SEC op2 = false → SEC ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##74: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq75 : ∀op2.eq_op SEI op2 = false → SEI ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##75: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq76 : ∀op2.eq_op SHA op2 = false → SHA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##76: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq77 : ∀op2.eq_op SLA op2 = false → SLA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##77: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq78 : ∀op2.eq_op STA op2 = false → STA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##78: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq79 : ∀op2.eq_op STHX op2 = false → STHX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##79: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq80 : ∀op2.eq_op STOP op2 = false → STOP ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##80: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq81 : ∀op2.eq_op STX op2 = false → STX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##81: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq82 : ∀op2.eq_op SUB op2 = false → SUB ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##82: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq83 : ∀op2.eq_op SWI op2 = false → SWI ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##83: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq84 : ∀op2.eq_op TAP op2 = false → TAP ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##84: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq85 : ∀op2.eq_op TAX op2 = false → TAX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##85: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq86 : ∀op2.eq_op TPA op2 = false → TPA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##86: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq87 : ∀op2.eq_op TST op2 = false → TST ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##87: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq88 : ∀op2.eq_op TSX op2 = false → TSX ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##88: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq89 : ∀op2.eq_op TXA op2 = false → TXA ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##89: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq90 : ∀op2.eq_op TXS op2 = false → TXS ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##90: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
+nlemma neqop_to_neq91 : ∀op2.eq_op WAIT op2 = false → WAIT ≠ op2. #op2; ncases op2; nnormalize; #H; ##[ ##91: napply  (bool_destruct … H) ##| ##*: #H1; napply False_ind; napply (opcode_destruct … H1) ##] nqed.
 
-nlemma eqop_to_eq : ∀op1,op2.eq_op op1 op2 = true → op1 = op2.
+nlemma neqop_to_neq : ∀op1,op2.eq_op op1 op2 = false → op1 ≠ op2.
  #op1; ncases op1;
- ##[ ##1: napply eqop_to_eq1 ##| ##2: napply eqop_to_eq2 ##| ##3: napply eqop_to_eq3 ##| ##4: napply eqop_to_eq4
- ##| ##5: napply eqop_to_eq5 ##| ##6: napply eqop_to_eq6 ##| ##7: napply eqop_to_eq7 ##| ##8: napply eqop_to_eq8
- ##| ##9: napply eqop_to_eq9 ##| ##10: napply eqop_to_eq10 ##| ##11: napply eqop_to_eq11 ##| ##12: napply eqop_to_eq12
- ##| ##13: napply eqop_to_eq13 ##| ##14: napply eqop_to_eq14 ##| ##15: napply eqop_to_eq15 ##| ##16: napply eqop_to_eq16
- ##| ##17: napply eqop_to_eq17 ##| ##18: napply eqop_to_eq18 ##| ##19: napply eqop_to_eq19 ##| ##20: napply eqop_to_eq20
- ##| ##21: napply eqop_to_eq21 ##| ##22: napply eqop_to_eq22 ##| ##23: napply eqop_to_eq23 ##| ##24: napply eqop_to_eq24
- ##| ##25: napply eqop_to_eq25 ##| ##26: napply eqop_to_eq26 ##| ##27: napply eqop_to_eq27 ##| ##28: napply eqop_to_eq28
- ##| ##29: napply eqop_to_eq29 ##| ##30: napply eqop_to_eq30 ##| ##31: napply eqop_to_eq31 ##| ##32: napply eqop_to_eq32
- ##| ##33: napply eqop_to_eq33 ##| ##34: napply eqop_to_eq34 ##| ##35: napply eqop_to_eq35 ##| ##36: napply eqop_to_eq36
- ##| ##37: napply eqop_to_eq37 ##| ##38: napply eqop_to_eq38 ##| ##39: napply eqop_to_eq39 ##| ##40: napply eqop_to_eq40
- ##| ##41: napply eqop_to_eq41 ##| ##42: napply eqop_to_eq42 ##| ##43: napply eqop_to_eq43 ##| ##44: napply eqop_to_eq44
- ##| ##45: napply eqop_to_eq45 ##| ##46: napply eqop_to_eq46 ##| ##47: napply eqop_to_eq47 ##| ##48: napply eqop_to_eq48
- ##| ##49: napply eqop_to_eq49 ##| ##50: napply eqop_to_eq50 ##| ##51: napply eqop_to_eq51 ##| ##52: napply eqop_to_eq52
- ##| ##53: napply eqop_to_eq53 ##| ##54: napply eqop_to_eq54 ##| ##55: napply eqop_to_eq55 ##| ##56: napply eqop_to_eq56
- ##| ##57: napply eqop_to_eq57 ##| ##58: napply eqop_to_eq58 ##| ##59: napply eqop_to_eq59 ##| ##60: napply eqop_to_eq60
- ##| ##61: napply eqop_to_eq61 ##| ##62: napply eqop_to_eq62 ##| ##63: napply eqop_to_eq63 ##| ##64: napply eqop_to_eq64
- ##| ##65: napply eqop_to_eq65 ##| ##66: napply eqop_to_eq66 ##| ##67: napply eqop_to_eq67 ##| ##68: napply eqop_to_eq68
- ##| ##69: napply eqop_to_eq69 ##| ##70: napply eqop_to_eq70 ##| ##71: napply eqop_to_eq71 ##| ##72: napply eqop_to_eq72
- ##| ##73: napply eqop_to_eq73 ##| ##74: napply eqop_to_eq74 ##| ##75: napply eqop_to_eq75 ##| ##76: napply eqop_to_eq76
- ##| ##77: napply eqop_to_eq77 ##| ##78: napply eqop_to_eq78 ##| ##79: napply eqop_to_eq79 ##| ##80: napply eqop_to_eq80
- ##| ##81: napply eqop_to_eq81 ##| ##82: napply eqop_to_eq82 ##| ##83: napply eqop_to_eq83 ##| ##84: napply eqop_to_eq84
- ##| ##85: napply eqop_to_eq85 ##| ##86: napply eqop_to_eq86 ##| ##87: napply eqop_to_eq87 ##| ##88: napply eqop_to_eq88
- ##| ##89: napply eqop_to_eq89 ##| ##90: napply eqop_to_eq90 ##| ##91: napply eqop_to_eq91 ##]
+ ##[ ##1: napply neqop_to_neq1 ##| ##2: napply neqop_to_neq2 ##| ##3: napply neqop_to_neq3 ##| ##4: napply neqop_to_neq4
+ ##| ##5: napply neqop_to_neq5 ##| ##6: napply neqop_to_neq6 ##| ##7: napply neqop_to_neq7 ##| ##8: napply neqop_to_neq8
+ ##| ##9: napply neqop_to_neq9 ##| ##10: napply neqop_to_neq10 ##| ##11: napply neqop_to_neq11 ##| ##12: napply neqop_to_neq12
+ ##| ##13: napply neqop_to_neq13 ##| ##14: napply neqop_to_neq14 ##| ##15: napply neqop_to_neq15 ##| ##16: napply neqop_to_neq16
+ ##| ##17: napply neqop_to_neq17 ##| ##18: napply neqop_to_neq18 ##| ##19: napply neqop_to_neq19 ##| ##20: napply neqop_to_neq20
+ ##| ##21: napply neqop_to_neq21 ##| ##22: napply neqop_to_neq22 ##| ##23: napply neqop_to_neq23 ##| ##24: napply neqop_to_neq24
+ ##| ##25: napply neqop_to_neq25 ##| ##26: napply neqop_to_neq26 ##| ##27: napply neqop_to_neq27 ##| ##28: napply neqop_to_neq28
+ ##| ##29: napply neqop_to_neq29 ##| ##30: napply neqop_to_neq30 ##| ##31: napply neqop_to_neq31 ##| ##32: napply neqop_to_neq32
+ ##| ##33: napply neqop_to_neq33 ##| ##34: napply neqop_to_neq34 ##| ##35: napply neqop_to_neq35 ##| ##36: napply neqop_to_neq36
+ ##| ##37: napply neqop_to_neq37 ##| ##38: napply neqop_to_neq38 ##| ##39: napply neqop_to_neq39 ##| ##40: napply neqop_to_neq40
+ ##| ##41: napply neqop_to_neq41 ##| ##42: napply neqop_to_neq42 ##| ##43: napply neqop_to_neq43 ##| ##44: napply neqop_to_neq44
+ ##| ##45: napply neqop_to_neq45 ##| ##46: napply neqop_to_neq46 ##| ##47: napply neqop_to_neq47 ##| ##48: napply neqop_to_neq48
+ ##| ##49: napply neqop_to_neq49 ##| ##50: napply neqop_to_neq50 ##| ##51: napply neqop_to_neq51 ##| ##52: napply neqop_to_neq52
+ ##| ##53: napply neqop_to_neq53 ##| ##54: napply neqop_to_neq54 ##| ##55: napply neqop_to_neq55 ##| ##56: napply neqop_to_neq56
+ ##| ##57: napply neqop_to_neq57 ##| ##58: napply neqop_to_neq58 ##| ##59: napply neqop_to_neq59 ##| ##60: napply neqop_to_neq60
+ ##| ##61: napply neqop_to_neq61 ##| ##62: napply neqop_to_neq62 ##| ##63: napply neqop_to_neq63 ##| ##64: napply neqop_to_neq64
+ ##| ##65: napply neqop_to_neq65 ##| ##66: napply neqop_to_neq66 ##| ##67: napply neqop_to_neq67 ##| ##68: napply neqop_to_neq68
+ ##| ##69: napply neqop_to_neq69 ##| ##70: napply neqop_to_neq70 ##| ##71: napply neqop_to_neq71 ##| ##72: napply neqop_to_neq72
+ ##| ##73: napply neqop_to_neq73 ##| ##74: napply neqop_to_neq74 ##| ##75: napply neqop_to_neq75 ##| ##76: napply neqop_to_neq76
+ ##| ##77: napply neqop_to_neq77 ##| ##78: napply neqop_to_neq78 ##| ##79: napply neqop_to_neq79 ##| ##80: napply neqop_to_neq80
+ ##| ##81: napply neqop_to_neq81 ##| ##82: napply neqop_to_neq82 ##| ##83: napply neqop_to_neq83 ##| ##84: napply neqop_to_neq84
+ ##| ##85: napply neqop_to_neq85 ##| ##86: napply neqop_to_neq86 ##| ##87: napply neqop_to_neq87 ##| ##88: napply neqop_to_neq88
+ ##| ##89: napply neqop_to_neq89 ##| ##90: napply neqop_to_neq90 ##| ##91: napply neqop_to_neq91 ##]
 nqed.
 
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
+nlemma neq_to_neqop1 : ∀op2.ADC ≠ op2 → eq_op ADC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop2 : ∀op2.ADD ≠ op2 → eq_op ADD op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop3 : ∀op2.AIS ≠ op2 → eq_op AIS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop4 : ∀op2.AIX ≠ op2 → eq_op AIX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop5 : ∀op2.AND ≠ op2 → eq_op AND op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop6 : ∀op2.ASL ≠ op2 → eq_op ASL op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop7 : ∀op2.ASR ≠ op2 → eq_op ASR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop8 : ∀op2.BCC ≠ op2 → eq_op BCC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop9 : ∀op2.BCLRn ≠ op2 → eq_op BCLRn op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop10 : ∀op2.BCS ≠ op2 → eq_op BCS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop11 : ∀op2.BEQ ≠ op2 → eq_op BEQ op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop12 : ∀op2.BGE ≠ op2 → eq_op BGE op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop13 : ∀op2.BGND ≠ op2 → eq_op BGND op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop14 : ∀op2.BGT ≠ op2 → eq_op BGT op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop15 : ∀op2.BHCC ≠ op2 → eq_op BHCC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop16 : ∀op2.BHCS ≠ op2 → eq_op BHCS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop17 : ∀op2.BHI ≠ op2 → eq_op BHI op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop18 : ∀op2.BIH ≠ op2 → eq_op BIH op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop19 : ∀op2.BIL ≠ op2 → eq_op BIL op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop20 : ∀op2.BIT ≠ op2 → eq_op BIT op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop21 : ∀op2.BLE ≠ op2 → eq_op BLE op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop22 : ∀op2.BLS ≠ op2 → eq_op BLS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop23 : ∀op2.BLT ≠ op2 → eq_op BLT op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop24 : ∀op2.BMC ≠ op2 → eq_op BMC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop25 : ∀op2.BMI ≠ op2 → eq_op BMI op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop26 : ∀op2.BMS ≠ op2 → eq_op BMS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop27 : ∀op2.BNE ≠ op2 → eq_op BNE op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop28 : ∀op2.BPL ≠ op2 → eq_op BPL op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop29 : ∀op2.BRA ≠ op2 → eq_op BRA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop30 : ∀op2.BRCLRn ≠ op2 → eq_op BRCLRn op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop31 : ∀op2.BRN ≠ op2 → eq_op BRN op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop32 : ∀op2.BRSETn ≠ op2 → eq_op BRSETn op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop33 : ∀op2.BSETn ≠ op2 → eq_op BSETn op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##33: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop34 : ∀op2.BSR ≠ op2 → eq_op BSR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##34: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop35 : ∀op2.CBEQA ≠ op2 → eq_op CBEQA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##35: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop36 : ∀op2.CBEQX ≠ op2 → eq_op CBEQX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##36: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop37 : ∀op2.CLC ≠ op2 → eq_op CLC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##37: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop38 : ∀op2.CLI ≠ op2 → eq_op CLI op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##38: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop39 : ∀op2.CLR ≠ op2 → eq_op CLR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##39: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop40 : ∀op2.CMP ≠ op2 → eq_op CMP op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##40: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop41 : ∀op2.COM ≠ op2 → eq_op COM op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##41: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop42 : ∀op2.CPHX ≠ op2 → eq_op CPHX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##42: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop43 : ∀op2.CPX ≠ op2 → eq_op CPX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##43: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop44 : ∀op2.DAA ≠ op2 → eq_op DAA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##44: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop45 : ∀op2.DBNZ ≠ op2 → eq_op DBNZ op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##45: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop46 : ∀op2.DEC ≠ op2 → eq_op DEC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##46: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop47 : ∀op2.DIV ≠ op2 → eq_op DIV op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##47: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop48 : ∀op2.EOR ≠ op2 → eq_op EOR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##48: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop49 : ∀op2.INC ≠ op2 → eq_op INC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##49: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop50 : ∀op2.JMP ≠ op2 → eq_op JMP op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##50: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop51 : ∀op2.JSR ≠ op2 → eq_op JSR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##51: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop52 : ∀op2.LDA ≠ op2 → eq_op LDA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##52: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop53 : ∀op2.LDHX ≠ op2 → eq_op LDHX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##53: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop54 : ∀op2.LDX ≠ op2 → eq_op LDX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##54: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop55 : ∀op2.LSR ≠ op2 → eq_op LSR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##55: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop56 : ∀op2.MOV ≠ op2 → eq_op MOV op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##56: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop57 : ∀op2.MUL ≠ op2 → eq_op MUL op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##57: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop58 : ∀op2.NEG ≠ op2 → eq_op NEG op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##58: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop59 : ∀op2.NOP ≠ op2 → eq_op NOP op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##59: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop60 : ∀op2.NSA ≠ op2 → eq_op NSA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##60: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop61 : ∀op2.ORA ≠ op2 → eq_op ORA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##61: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop62 : ∀op2.PSHA ≠ op2 → eq_op PSHA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##62: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop63 : ∀op2.PSHH ≠ op2 → eq_op PSHH op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##63: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop64 : ∀op2.PSHX ≠ op2 → eq_op PSHX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##64: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop65 : ∀op2.PULA ≠ op2 → eq_op PULA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##65: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop66 : ∀op2.PULH ≠ op2 → eq_op PULH op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##66: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop67 : ∀op2.PULX ≠ op2 → eq_op PULX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##67: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop68 : ∀op2.ROL ≠ op2 → eq_op ROL op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##68: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop69 : ∀op2.ROR ≠ op2 → eq_op ROR op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##69: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop70 : ∀op2.RSP ≠ op2 → eq_op RSP op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##70: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop71 : ∀op2.RTI ≠ op2 → eq_op RTI op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##71: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop72 : ∀op2.RTS ≠ op2 → eq_op RTS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##72: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop73 : ∀op2.SBC ≠ op2 → eq_op SBC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##73: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop74 : ∀op2.SEC ≠ op2 → eq_op SEC op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##74: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop75 : ∀op2.SEI ≠ op2 → eq_op SEI op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##75: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop76 : ∀op2.SHA ≠ op2 → eq_op SHA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##76: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop77 : ∀op2.SLA ≠ op2 → eq_op SLA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##77: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop78 : ∀op2.STA ≠ op2 → eq_op STA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##78: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop79 : ∀op2.STHX ≠ op2 → eq_op STHX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##79: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop80 : ∀op2.STOP ≠ op2 → eq_op STOP op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##80: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop81 : ∀op2.STX ≠ op2 → eq_op STX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##81: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop82 : ∀op2.SUB ≠ op2 → eq_op SUB op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##82: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop83 : ∀op2.SWI ≠ op2 → eq_op SWI op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##83: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop84 : ∀op2.TAP ≠ op2 → eq_op TAP op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##84: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop85 : ∀op2.TAX ≠ op2 → eq_op TAX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##85: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop86 : ∀op2.TPA ≠ op2 → eq_op TPA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##86: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop87 : ∀op2.TST ≠ op2 → eq_op TST op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##87: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop88 : ∀op2.TSX ≠ op2 → eq_op TSX op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##88: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop89 : ∀op2.TXA ≠ op2 → eq_op TXA op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##89: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop90 : ∀op2.TXS ≠ op2 → eq_op TXS op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##90: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
+nlemma neq_to_neqop91 : ∀op2.WAIT ≠ op2 → eq_op WAIT op2 = false. #op2; ncases op2; nnormalize; #H; ##[ ##91: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##] nqed.
 
-nlemma eq_to_eqop : ∀op1,op2.op1 = op2 → eq_op op1 op2 = true.
+nlemma neq_to_neqop : ∀op1,op2.op1 ≠ op2 → eq_op op1 op2 = false.
  #op1; ncases op1;
- ##[ ##1: napply eq_to_eqop1 ##| ##2: napply eq_to_eqop2 ##| ##3: napply eq_to_eqop3 ##| ##4: napply eq_to_eqop4
- ##| ##5: napply eq_to_eqop5 ##| ##6: napply eq_to_eqop6 ##| ##7: napply eq_to_eqop7 ##| ##8: napply eq_to_eqop8
- ##| ##9: napply eq_to_eqop9 ##| ##10: napply eq_to_eqop10 ##| ##11: napply eq_to_eqop11 ##| ##12: napply eq_to_eqop12
- ##| ##13: napply eq_to_eqop13 ##| ##14: napply eq_to_eqop14 ##| ##15: napply eq_to_eqop15 ##| ##16: napply eq_to_eqop16
- ##| ##17: napply eq_to_eqop17 ##| ##18: napply eq_to_eqop18 ##| ##19: napply eq_to_eqop19 ##| ##20: napply eq_to_eqop20
- ##| ##21: napply eq_to_eqop21 ##| ##22: napply eq_to_eqop22 ##| ##23: napply eq_to_eqop23 ##| ##24: napply eq_to_eqop24
- ##| ##25: napply eq_to_eqop25 ##| ##26: napply eq_to_eqop26 ##| ##27: napply eq_to_eqop27 ##| ##28: napply eq_to_eqop28
- ##| ##29: napply eq_to_eqop29 ##| ##30: napply eq_to_eqop30 ##| ##31: napply eq_to_eqop31 ##| ##32: napply eq_to_eqop32
- ##| ##33: napply eq_to_eqop33 ##| ##34: napply eq_to_eqop34 ##| ##35: napply eq_to_eqop35 ##| ##36: napply eq_to_eqop36
- ##| ##37: napply eq_to_eqop37 ##| ##38: napply eq_to_eqop38 ##| ##39: napply eq_to_eqop39 ##| ##40: napply eq_to_eqop40
- ##| ##41: napply eq_to_eqop41 ##| ##42: napply eq_to_eqop42 ##| ##43: napply eq_to_eqop43 ##| ##44: napply eq_to_eqop44
- ##| ##45: napply eq_to_eqop45 ##| ##46: napply eq_to_eqop46 ##| ##47: napply eq_to_eqop47 ##| ##48: napply eq_to_eqop48
- ##| ##49: napply eq_to_eqop49 ##| ##50: napply eq_to_eqop50 ##| ##51: napply eq_to_eqop51 ##| ##52: napply eq_to_eqop52
- ##| ##53: napply eq_to_eqop53 ##| ##54: napply eq_to_eqop54 ##| ##55: napply eq_to_eqop55 ##| ##56: napply eq_to_eqop56
- ##| ##57: napply eq_to_eqop57 ##| ##58: napply eq_to_eqop58 ##| ##59: napply eq_to_eqop59 ##| ##60: napply eq_to_eqop60
- ##| ##61: napply eq_to_eqop61 ##| ##62: napply eq_to_eqop62 ##| ##63: napply eq_to_eqop63 ##| ##64: napply eq_to_eqop64
- ##| ##65: napply eq_to_eqop65 ##| ##66: napply eq_to_eqop66 ##| ##67: napply eq_to_eqop67 ##| ##68: napply eq_to_eqop68
- ##| ##69: napply eq_to_eqop69 ##| ##70: napply eq_to_eqop70 ##| ##71: napply eq_to_eqop71 ##| ##72: napply eq_to_eqop72
- ##| ##73: napply eq_to_eqop73 ##| ##74: napply eq_to_eqop74 ##| ##75: napply eq_to_eqop75 ##| ##76: napply eq_to_eqop76
- ##| ##77: napply eq_to_eqop77 ##| ##78: napply eq_to_eqop78 ##| ##79: napply eq_to_eqop79 ##| ##80: napply eq_to_eqop80
- ##| ##81: napply eq_to_eqop81 ##| ##82: napply eq_to_eqop82 ##| ##83: napply eq_to_eqop83 ##| ##84: napply eq_to_eqop84
- ##| ##85: napply eq_to_eqop85 ##| ##86: napply eq_to_eqop86 ##| ##87: napply eq_to_eqop87 ##| ##88: napply eq_to_eqop88
- ##| ##89: napply eq_to_eqop89 ##| ##90: napply eq_to_eqop90 ##| ##91: napply eq_to_eqop91 ##]
+ ##[ ##1: napply neq_to_neqop1 ##| ##2: napply neq_to_neqop2 ##| ##3: napply neq_to_neqop3 ##| ##4: napply neq_to_neqop4
+ ##| ##5: napply neq_to_neqop5 ##| ##6: napply neq_to_neqop6 ##| ##7: napply neq_to_neqop7 ##| ##8: napply neq_to_neqop8
+ ##| ##9: napply neq_to_neqop9 ##| ##10: napply neq_to_neqop10 ##| ##11: napply neq_to_neqop11 ##| ##12: napply neq_to_neqop12
+ ##| ##13: napply neq_to_neqop13 ##| ##14: napply neq_to_neqop14 ##| ##15: napply neq_to_neqop15 ##| ##16: napply neq_to_neqop16
+ ##| ##17: napply neq_to_neqop17 ##| ##18: napply neq_to_neqop18 ##| ##19: napply neq_to_neqop19 ##| ##20: napply neq_to_neqop20
+ ##| ##21: napply neq_to_neqop21 ##| ##22: napply neq_to_neqop22 ##| ##23: napply neq_to_neqop23 ##| ##24: napply neq_to_neqop24
+ ##| ##25: napply neq_to_neqop25 ##| ##26: napply neq_to_neqop26 ##| ##27: napply neq_to_neqop27 ##| ##28: napply neq_to_neqop28
+ ##| ##29: napply neq_to_neqop29 ##| ##30: napply neq_to_neqop30 ##| ##31: napply neq_to_neqop31 ##| ##32: napply neq_to_neqop32
+ ##| ##33: napply neq_to_neqop33 ##| ##34: napply neq_to_neqop34 ##| ##35: napply neq_to_neqop35 ##| ##36: napply neq_to_neqop36
+ ##| ##37: napply neq_to_neqop37 ##| ##38: napply neq_to_neqop38 ##| ##39: napply neq_to_neqop39 ##| ##40: napply neq_to_neqop40
+ ##| ##41: napply neq_to_neqop41 ##| ##42: napply neq_to_neqop42 ##| ##43: napply neq_to_neqop43 ##| ##44: napply neq_to_neqop44
+ ##| ##45: napply neq_to_neqop45 ##| ##46: napply neq_to_neqop46 ##| ##47: napply neq_to_neqop47 ##| ##48: napply neq_to_neqop48
+ ##| ##49: napply neq_to_neqop49 ##| ##50: napply neq_to_neqop50 ##| ##51: napply neq_to_neqop51 ##| ##52: napply neq_to_neqop52
+ ##| ##53: napply neq_to_neqop53 ##| ##54: napply neq_to_neqop54 ##| ##55: napply neq_to_neqop55 ##| ##56: napply neq_to_neqop56
+ ##| ##57: napply neq_to_neqop57 ##| ##58: napply neq_to_neqop58 ##| ##59: napply neq_to_neqop59 ##| ##60: napply neq_to_neqop60
+ ##| ##61: napply neq_to_neqop61 ##| ##62: napply neq_to_neqop62 ##| ##63: napply neq_to_neqop63 ##| ##64: napply neq_to_neqop64
+ ##| ##65: napply neq_to_neqop65 ##| ##66: napply neq_to_neqop66 ##| ##67: napply neq_to_neqop67 ##| ##68: napply neq_to_neqop68
+ ##| ##69: napply neq_to_neqop69 ##| ##70: napply neq_to_neqop70 ##| ##71: napply neq_to_neqop71 ##| ##72: napply neq_to_neqop72
+ ##| ##73: napply neq_to_neqop73 ##| ##74: napply neq_to_neqop74 ##| ##75: napply neq_to_neqop75 ##| ##76: napply neq_to_neqop76
+ ##| ##77: napply neq_to_neqop77 ##| ##78: napply neq_to_neqop78 ##| ##79: napply neq_to_neqop79 ##| ##80: napply neq_to_neqop80
+ ##| ##81: napply neq_to_neqop81 ##| ##82: napply neq_to_neqop82 ##| ##83: napply neq_to_neqop83 ##| ##84: napply neq_to_neqop84
+ ##| ##85: napply neq_to_neqop85 ##| ##86: napply neq_to_neqop86 ##| ##87: napply neq_to_neqop87 ##| ##88: napply neq_to_neqop88
+ ##| ##89: napply neq_to_neqop89 ##| ##90: napply neq_to_neqop90 ##| ##91: napply neq_to_neqop91 ##]
 nqed.