proposition: Lemma map_inj_in_uniq s : {in s &, injective f} -> uniq (map f s) = uniq s.
proof: Proof. elim: s => //= x s IHs //= injf; congr (~~ _ && _). apply/mapP/idP=> [[y sy /injf] | ]; last by exists x. by rewrite mem_head mem_behead // => ->. by apply: IHs => y z sy sz; apply: injf => //; apply: predU1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)