proposition: Lemma map_fmap_mono {A B} (f : A → B) (m1 m2 : M A) : m1 ⊆ m2 → f <$> m1 ⊆ f <$> m2.
proof: Proof. rewrite !map_subseteq_spec; intros Hm i x. rewrite !lookup_fmap, !fmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)