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