proposition: Lemma imfsetP (T : choiceType) (f : T -> K) (p : finmempred T) (k : K) : reflect (exists2 x : T, in_mem x p & k = f x) (k \in imfset key f p).
proof: Proof. rewrite unlock seq_fsetE /=; apply: (iffP mapP) => [] [x xp eqkf]; by exists x => //=; move: xp; rewrite enum_finmemE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)