proposition: Lemma seq_masks_uniq : uniq w -> uniq [seq mask (val m) w | m : (size w).-tuple bool].
proof: Proof. move=> w_uniq; rewrite map_inj_uniq; first exact: enum_uniq. exact/mask_injP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted