proposition: Lemma card_imfset (T T' : choiceType) (f : T -> T') (p : finmempred _) : injective f -> #|` (imfset key f p)| = size (enum_finmem p).
proof: Proof. by move=> f_inj; rewrite card_in_imfset //= => x y ? ?; apply: f_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)