proposition: Lemma map_zip_with_map_zip {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) : map_zip_with f m1 m2 = uncurry f <$> map_zip 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)