proposition: Lemma enum_sub_undupE : map val (enum undup_finType) = undup subenum.
proof: Proof. rewrite enumT unlock /= -{2}(subType_seqP TP subenumP). by rewrite (undup_map_inj val_inj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools