proposition: Lemma finite_sub_undupP : Finite.axiom (undup (subType_seq TP subenum)).
proof: Proof. move=> x; rewrite count_uniq_mem; last exact: undup_uniq. rewrite mem_undup; have /= := subenum_in (valP x). by rewrite -{1}(subType_seqP TP subenumP) (mem_map val_inj) => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools