proposition: Lemma zip_map_snd {A B C} (a: list A) (b: list B) (f: B → C): zip a (map f b) = map (second f) (zip a b).
proof: Proof. Proof with auto. revert b. induction a; destruct b... simpl in *. intros. rewrite IHa... Qed.
imports: Coq.Lists.List Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms CoRN.stdlib_omissions.Pair