proposition: Lemma card_in_imfset (T T' : choiceType) (f : T -> T') (p : finmempred T) : {in p &, injective f} -> #|` (imfset key f p)| = (size (enum_finmem p)).
proof: Proof. move=> f_inj; rewrite unlock /= size_seq_fset undup_id ?size_map//. rewrite map_inj_in_uniq ?enum_finmem_uniq// => ??. by rewrite !enum_finmemE; apply: f_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)