proposition: Lemma perm_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2.
proof: Proof. by move=> eq_s12; apply/eq_uniq; [apply/perm_size | apply/perm_mem]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)