proposition: Lemma set_omap_empty_iff f X : set_omap f X ≡ ∅ ↔ set_Forall (λ x, f x = None) X.
proof: Proof. split; set_unfold; unfold set_Forall. - intros Hi x Hx. destruct (f x) as [y|] eqn:Hy; naive_solver. - intros Hi y (x & Hf & Hx). specialize (Hi x Hx). by rewrite Hi in Hf. Qed.
imports: stdpp(relations) stdpp(options)