proposition: Lemma mkFinPredType_of_subproof (T : eqType) (pT : predType T) (fpred_seq : pT -> seq T) (pred_fsetE : forall p, fpred_seq p =i p) : forall p x, x \in fpred_seq p = topred p x.
proof: Proof. by move=> p x; rewrite topredE pred_fsetE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)