proposition: Lemma perm_zip2 {S T : eqType} (s1 s2 : seq S) (t1 t2 : seq T) : size s1 = size t1 -> size s2 = size t2 -> perm_eq (zip s1 t1) (zip s2 t2) -> perm_eq t1 t2.
proof: Proof. by move=> ? ? ?; rewrite (@perm_zip1 _ _ s1 s2) 1?perm_zip_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)