proposition: Lemma to_maskK : cancel to_mask (fun m => Subseqs (mask_subseq (val m) w)).
proof: Proof. by rewrite /to_mask => s; case: to_mask_spec => m /eqP eqm; apply val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted