proposition: Lemma tuto_eq_from_tnth : forall (t1 t2 : n.-tuple T), tnth t1 =1 tnth t2 -> t1 = t2.
proof: Proof. move=> *; apply: val_inj; rewrite /= -2!map_tnth_enum; exact: eq_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)