proposition: Lemma elem_of_set_omap f X y : y ∈ set_omap f X ↔ ∃ x, x ∈ X ∧ f x = Some y.
proof: Proof. unfold set_omap. rewrite elem_of_list_to_set, elem_of_list_omap. by setoid_rewrite elem_of_elements. Qed.
imports: stdpp(relations) stdpp(options)