proposition: Lemma Subseqs_maskK : uniq w -> cancel (fun m => Subseqs (mask_subseq (val m) w)) to_mask.
proof: Proof. rewrite /to_mask=> w_uniq m; case: to_mask_spec => m' /= /eqP. exact/mask_injP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted