proposition: Lemma tnthL (T:eqType) (x z : seq T) (i : 'I_(size x)) (j : 'I_(size (x++z))) : i = j :> nat -> tnth (in_tuple x) i = tnth (in_tuple (x++z)) j.
proof: Proof. move => e. pose a := tnth (in_tuple x) i. by rewrite !(tnth_nth a) /= -e nth_cat ltn_ord. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)