proposition: Lemma mem_imfset (T : choiceType) (f : T -> K) (p : finmempred T) : injective f -> forall (x : T), (f x \in imfset key f p) = (in_mem x p).
proof: Proof. by move=> f_inj x; rewrite unlock seq_fsetE mem_map// enum_finmemE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)