fact: Parameter imfset : forall (key : unit) (T K : choiceType) (f : T -> K) (p : finmempred T), phantom (mem_pred T) p -> {fset K}.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)