proposition: Lemma perm_undup s1 s2 : s1 =i s2 -> perm_eq (undup s1) (undup s2).
proof: Proof. by move=> Es12; rewrite uniq_perm ?undup_uniq // => s; rewrite !mem_undup. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)