proposition: Lemma big_fset1 (a : I) (F : [fset a] -> R) : \big[op/idx]_(i : [fset a]) F i = F [` fset11 a].
proof: Proof. by rewrite /index_enum -enumT enum_fset1 big_seq1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)