proposition: Lemma bind_Some_equiv {A} `{Equiv B} (f : A → option B) (mx : option A) y : mx ≫= f ≡ Some y ↔ ∃ x, mx = Some x ∧ f x ≡ Some y.
proof: Proof. destruct mx; split; first [by inv 1|naive_solver]. Qed.
imports: stdpp(options)