proposition: Lemma set_omap_filter_L P `{∀ x, Decision (P x)} f X : (∀ x, x ∈ X → is_Some (f x) → P x) → set_omap f (filter P X) = set_omap f X.
proof: Proof. unfold_leibniz. apply set_omap_filter. Qed.
imports: stdpp(relations) stdpp(options)