proposition: Lemma big_fset_seq_cond (T : choiceType) (J : {fset T}) P F : \big[*%M/1]_(x : J | P (val x)) F (val x) = \big[*%M/1]_(x <- enum_fset J | P x) F x.
proof: Proof. case: J=> J c; rewrite -(big_map val) /index_enum. by rewrite !unlock val_fset_sub_enum ?canonical_uniq. Qed.
imports: mathcomp(all_ssreflect all_algebra)