proposition: Lemma finite_subP : Finite.axiom subType_seq.
proof: Proof. move=> xP; rewrite (eq_count (a2 := (pred1 (val xP)) \o val)). - by rewrite -count_map subType_seqP subenum_countE //=; exact: valP. - by move=> i; apply/idP/idP=> /eqP H; apply/eqP; [rewrite H | apply val_inj]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools