Theorem: Option.isNone_eq_true (RegMachine/Imported.lean)

State before:
α : Type u_1
o : Option α
⊢ isNone o = true ↔ o = none
Tactic:
cases o <;> simp
State after:
no goals