proposition: Lemma map_fmap_zip {A' A B' B} (g1 : A' → A) (g2 : B' → B) (m1 : M A') (m2 : M B') : map_zip (fmap g1 m1) (fmap g2 m2) = prod_map g1 g2 <$> map_zip m1 m2.
proof: Proof. rewrite map_zip_with_fmap, map_zip_with_map_zip. generalize (map_zip m1 m2); intro m. apply map_eq; intro i. by rewrite !lookup_fmap; destruct (m !! i) as [[x1 x2]|]. Qed.
imports: Coq(Permutation) stdpp(options)