proposition: Lemma zip_map2 {P Q R S} (f : P -> R) (g : Q -> S) (s1 : seq P) (s2 : seq Q) : zip (map f s1) (map g s2) = map (fun '(x1,x2) => (f x1,g x2)) (zip s1 s2).
proof: Proof. elim: s1 s2=>/= [|x1 s1 IH] [|x2 s2] //=. by congr cons. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)