proposition: Lemma big_seq_fset (T : choiceType) (s : seq T) F : uniq s -> \big[*%M/1]_(x : [fset x in s]) F (val x) = \big[*%M/1]_(x <- s) F x.
proof: Proof. by apply/big_seq_fset_cond. Qed.
imports: mathcomp(all_ssreflect all_algebra)