proposition: Lemma map_agree_omap {A B} (f : A → option B) (m1 m2 : M A) : map_agree m1 m2 → map_agree (omap f m1) (omap f m2).
proof: Proof. rewrite !map_agree_spec. setoid_rewrite lookup_omap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)