-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 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.