efinition all_words n T (alphabet : seq T) :=
  let prepend x wl := [seq x :: w | w <- wl] in
  let extend wl := flatten [seq prepend x wl | x <- alphabet] in
  iter n extend [::[::]].

Definition tuple_enum (T : finType) n : seq (n.-tuple T) :=
  pmap insub (all_words n (enum T)).

Lemma enumP T n : Finite.axiom (tuple_enum T n).
Admitted.

Definition tuple_finMixin n T := Eval hnf in FinMixin (@enumP T n).
Canonical tuple_finType n (T : finType) :=
  Eval hnf in FinType (n.-tuple T) (@tuple_finMixin n T).