proposition: Lemma tuto_map_tnth_enum : forall (t : n.-tuple T), map (tnth t) (enum 'I_n) = t.
proof: Proof. move=> t; case def_t: {-}(val t) => [|x0 t']. by rewrite [enum _]size0nil // -cardE card_ord -(size_tuple t) def_t. apply: (@eq_from_nth _ x0) => [|i]; rewrite size_map. by rewrite -cardE size_tuple card_ord. move=> lt_i_e; have lt_i_n: i < n by rewrite -cardE card_ord in lt_i_e. by rewrite (nth_map (Ordinal lt_i_n)) // (tnth_nth x0) nth_enum_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)