Theorem: Option.bind_const_none (Etch/Verification/Misc.lean)

State before:
α : Type u_1
β : Type u_2
x : Option α
⊢ (Option.bind x fun x => none) = none
Tactic:
cases x <;> simp
State after:
no goals