proposition: Lemma map_fmap_strict_mono {A B} (f : A → B) (m1 m2 : M A) : m1 ⊂ m2 → f <$> m1 ⊂ f <$> m2.
proof: Proof. rewrite !map_subset_alt. intros [? (j&?&?)]; split; auto using map_fmap_mono. exists j. by rewrite !lookup_fmap, fmap_None, fmap_is_Some. Qed.
imports: Coq(Permutation) stdpp(options)