proposition: Lemma undup_cat s t : undup (s ++ t) = [seq x <- undup s | x \notin t] ++ undup t.
proof: Proof. by elim: s => //= x s ->; rewrite mem_cat; do 2 case: in_mem => //=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)