proposition: Lemma enum_imfset (T : choiceType) (f : T -> K) (p : finmempred T) : {in p &, injective f} -> perm_eq (imfset key f p) [seq f x | x <- enum_finmem p].
proof: Proof. move=> f_inj; rewrite unlock -[X in perm_eq _ X]undup_id ?seq_fset_perm//. 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)