proposition: Lemma big_subseqs_cond (P : pred (seq T)) (F : seq T -> R) (s : seq T) : uniq s -> \big[*%M/1]_(i : subseqs s | P i) F i = \big[*%M/1]_(m : (size s).-tuple bool | P (mask m s)) F (mask m s).
proof: Proof. move=> suniq; rewrite [LHS]big_mkcond [RHS]big_mkcond. exact: (big_subseqs (fun i => if P i then F i else 1)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted