proposition: Lemma big_seq_fset_cond (T : choiceType) (s : seq T) P F : uniq s -> \big[*%M/1]_(x : [fset x in s] | P (val x)) F (val x) = \big[*%M/1]_(x <- s | P x) F x.
proof: Proof. move=> eq_s; rewrite big_fset_seq_cond; apply/perm_big. by apply/uniq_perm=> //= x; rewrite in_fset. Qed.
imports: mathcomp(all_ssreflect all_algebra)