proposition: Lemma perm_zip1 {S T : eqType} (t1 t2 : seq T) (s1 s2 : seq S): size s1 = size t1 -> size s2 = size t2 -> perm_eq (zip s1 t1) (zip s2 t2) -> perm_eq s1 s2.
proof: Proof. wlog [x y] : s1 s2 t1 t2 / (S * T)%type => [hwlog|]. case: s2 t2 => [|x s2] [|y t2] //; last exact: hwlog. by case: s1 t1 => [|u s1] [|v t1]//= _ _ /perm_nilP. move=> eq1 eq2 /(perm_iotaP (x, y))[ns nsP /(congr1 (@unzip1 _ _))]. rewrite unzip1_zip ?unzip1_map_nth_zip -?eq1// => ->. by apply/(perm_iotaP x); exists ns; rewrite // size_zip -eq2 minnn in nsP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)