proposition: Lemma size_enum : size enum = #|T| ^ n.
proof: Proof. rewrite /= cardE size_pmap_sub; elim: n => //= m IHm. rewrite expnS /codom /image_mem; elim: {2 3}(fintype.enum T) => //= x e IHe. by rewrite count_cat {}IHe count_map IHm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)