proposition: Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y : f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
proof: Proof. destruct mx; simpl; split. - intros ?%(inj Some). eauto. - intros (? & ->%(inj Some) & ?). constructor. done. - intros [=]%symmetry%None_equiv_eq. - intros (? & [=] & ?). Qed.
imports: stdpp(options)