proposition: Lemma eq_from_tnth t1 t2 : tnth t1 =1 tnth t2 -> t1 = t2.
proof: Proof. by move/eq_map=> eq_t; apply: val_inj; rewrite /= -!map_tnth_enum eq_t. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)