proposition: Lemma uniq_perm s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.
proof: Proof. move=> Us1 Us2 eq12; apply/allP=> x _; apply/eqP. by rewrite !count_uniq_mem ?eq12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)