Theorem: Option.forall_ne_some (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
o : Option α
⊢ (∀ (a : α), o ≠ some a) ↔ o = none
Tactic:
cases o <;> simp
State after:
no goals