fact: Definition helper o (mr : AllowModify (labelCount o)) o' (orig : AllowModify (labelCount o')) : AllowModify (labelCount o') := match opCode_eq_dec o o' with | left h => eq_rec_r _ (fun x => x) h mr | right _ => orig end.
imports: QuickChick.ifcbasic(Rules Machine) List