proposition: Lemma rev_uniq s : uniq (rev s) = uniq s.
proof: Proof. elim: s => // x s IHs. by rewrite rev_cons -cats1 cat_uniq /= andbT andbC mem_rev orbF IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)