ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##30: #H; napply (λx:P.x)
ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##30: #H; napply (λx:P.x)