proposition: Lemma mem_undup s : undup s =i s.
proof: Proof. move=> x; elim: s => //= y s IHs. by case s_y: (y \in s); rewrite !inE IHs //; case: eqP => [->|]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)