proposition: Lemma map_agree_fmap {A B} (f : A → B) (m1 m2 : M A) `{!Inj (=) (=) f}: map_agree (f <$> m1) (f <$> m2) ↔ map_agree m1 m2.
proof: Proof. naive_solver eauto using map_agree_fmap_1, map_agree_fmap_2. Qed.
imports: Coq(Permutation) stdpp(options)