proposition: Lemma map_fmap_difference {A B} (f : A → B) (m1 m2 : M A) : f <$> (m1 ∖ m2) = (f <$> m1) ∖ (f <$> m2).
proof: Proof. apply map_eq. intros i. rewrite !lookup_difference, !lookup_fmap, !lookup_difference. destruct (m1 !! i), (m2 !! i); done. Qed.
imports: Coq(Permutation) stdpp(options)