proposition: Lemma map_disjoint_omap {A B} (f1 f2 : A → option B) (m1 m2 : M A) : m1 ##ₘ m2 → omap f1 m1 ##ₘ omap f2 m2.
proof: Proof. rewrite !map_disjoint_spec. setoid_rewrite lookup_omap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)