proposition: Lemma map_fmap_zip_with {A B C D} (f : A → B → C) (g : C → D) (m1 : M A) (m2 : M B) : g <$> map_zip_with f m1 m2 = map_zip_with (λ x y, g (f x y)) m1 m2.
proof: Proof. apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)