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