proposition: Lemma map_agree_fmap_1 {A B} (f : A → B) (m1 m2 : M A) `{!Inj (=) (=) f}: map_agree (f <$> m1) (f <$> m2) → map_agree m1 m2.
proof: Proof. rewrite !map_agree_spec. setoid_rewrite lookup_fmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)