proposition: Lemma subseqs_masks_uniq : uniq w -> uniq [seq Subseqs (mask_subseq (val m) w) | m : (size w).-tuple bool].
proof: Proof. move /seq_masks_uniq => s_uniq. by rewrite -(map_inj_uniq val_inj) -map_comp. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted