proposition: Lemma cat_uniq s1 s2 : uniq (s1 ++ s2) = [&& uniq s1, ~~ has [in s1] s2 & uniq s2].
proof: Proof. elim: s1 => [|x s1 IHs]; first by rewrite /= has_pred0. by rewrite has_sym /= mem_cat !negb_or has_sym IHs -!andbA; do !bool_congr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)