proposition: Lemma map_zip_with_fmap_1 {A' A B C} (f : A → B → C) (g : A' → A) (m1 : M A') (m2 : M B) : map_zip_with f (g <$> m1) m2 = map_zip_with (λ x y, f (g x) y) m1 m2.
proof: Proof. rewrite <- (map_fmap_id m2) at 1. by rewrite map_zip_with_fmap. Qed.
imports: Coq(Permutation) stdpp(options)