fact: Definition pred_of_finset (K : choiceType) (f : finSet K) : pred K := fun k => k \in (enum_fset f).
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)