proposition: Lemma map_disjoint_fmap {A B} (f1 f2 : A → B) (m1 m2 : M A) : f1 <$> m1 ##ₘ f2 <$> m2 ↔ m1 ##ₘ m2.
proof: Proof. rewrite !map_disjoint_spec. setoid_rewrite lookup_fmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)