proposition: Lemma eq_map_all I (T : eqType) (f g : I -> T) (s : seq I) : (map f s == map g s) = all [pred xy | xy.1 == xy.2] [seq (f i, g i) | i <- s].
proof: Proof. by rewrite eqseq_all all2E !size_map eqxx zip_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)