proposition: Lemma map_omap_union {A B} (f : A → option B) (m1 m2 : M A) : m1 ##ₘ m2 → omap f (m1 ∪ m2) = omap f m1 ∪ omap f m2.
proof: Proof. intros Hdisj. apply map_eq; intros i. specialize (Hdisj i). apply option_eq; intros x. rewrite lookup_omap, !lookup_union, !lookup_omap. destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)