proposition: Lemma dom_omap_subseteq {A B} (f : A → option B) (m : M A) : dom (omap f m) ⊆ dom m.
proof: Proof. intros a. rewrite !elem_of_dom. intros [c Hm]. apply lookup_omap_Some in Hm. naive_solver. Qed.
imports: stdpp(options)