proposition: Lemma to_mask_spec s : {m : (size w).-tuple bool | mask m w == s}.
proof: Proof. move: s => [s subs]; apply/sigW => /=. by move: subs => /subseqP[m /eqP szm ->{s}]; exists (Tuple szm). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted