proposition: Lemma fsfun_injective_inP f (T : {fset K}) : reflect {in T &, injective f} (injectiveb [ffun x : T => f (val x)]).
proof: Proof. apply: (iffP (@injectiveP _ _ _)) => f_inj a b; last first. by rewrite !ffunE => *; apply: val_inj; apply: f_inj => //; apply: valP. move=> aT bT eq_ga_gb; have := f_inj.[aT].[bT]; rewrite !ffunE /=. by move=> /(_ eq_ga_gb) /(congr1 val). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)