proposition: Lemma card_inj_ffuns_on D T (R : pred T) : #|[set f : {ffun D -> T} in ffun_on R | injectiveb f]| = #|R| ^_ #|D|.
proof: Proof. rewrite -card_uniq_tuples. have bijFF: {on (_ : pred _), bijective (@Finfun D T)}. by exists fgraph => x _; [apply: FinfunK | apply: fgraphK]. rewrite -(on_card_preimset (bijFF _)); apply: eq_card => /= t. rewrite !inE -(big_andE predT) -big_image /= big_all. by rewrite -[t in RHS]FinfunK -codom_ffun. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)