proposition: Lemma big_subseqs_undup (F : seq T -> R) (s : seq T) : idempotent op -> \big[*%M/1]_(i : subseqs s) F i = \big[*%M/1]_(m : (size s).-tuple bool) F (mask m s).
proof: Proof. move=> opid; rewrite -big_enum. rewrite (perm_big _ (enum_subseqsE s)) big_undup //. by rewrite big_map big_enum; exact: eq_bigr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted