proposition: Lemma val_enum_subseqs : perm_eq (map val (enum {: subseqs})) (undup [seq mask (val m) w | m : (size w).-tuple bool]).
proof: Proof. have /permPl -> := perm_map val enum_subseqsE. rewrite -(undup_map_inj val_inj) -map_comp. exact: (eq_ind _ (perm_eq _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted