proposition: Lemma big_seq_fsetE (X : {fset I}) (P : pred I) (F : I -> R) : \big[op/idx]_(i <- X | P i) F i = \big[op/idx]_(x : X | P (val x)) F (val x).
proof: Proof. by rewrite enum_fsetE big_map enumT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)