proposition: Lemma big_subseqs_undup_cond (F : seq T -> R) (P : pred (seq T)) (s : seq T) : idempotent op -> \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=> opid; rewrite big_mkcond /=. by rewrite (big_subseqs_undup (fun i => if P i then F i else 1)) -?big_mkcond. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted