proposition: Lemma enum_subseqsE : perm_eq (enum {: subseqs}) (undup [seq Subseqs (mask_subseq (val m) w) | m : (size w).-tuple bool]).
proof: Proof. apply: uniq_perm; [exact: enum_uniq | exact: undup_uniq |]. move=> [s subs] /=; rewrite mem_enum inE mem_undup. apply/esym/mapP; have /subseqP[m /eqP szm eqs] := subs. by exists (Tuple szm); [exact: mem_enum | exact: val_inj]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted