proposition: Lemma tnthS x t i : tnth [tuple of x :: t] (lift ord0 i) = tnth t i.
proof: Proof. by rewrite (tnth_nth (tnth_default t i)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)