proposition: Lemma map_uniq s : uniq (map f s) -> uniq s.
proof: Proof. elim: s => //= x s IHs /andP[not_sfx /IHs->]; rewrite andbT. by apply: contra not_sfx => sx; apply/mapP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)