proposition: Lemma run_trans x p r i (Hi : i < size x) : nfa_run x p r -> nth p (p::r) i.+1 \in nfa_trans (nth p (p::r) i) (tnth (in_tuple x) (Ordinal Hi)).
proof: Proof. move => H. elim: H i Hi => {x p r} // a p q x r tr run IH /= [|i] Hi //. rewrite !(set_nth_default q); try by rewrite /= -(run_size run) // ltnW. rewrite {1}[nth]lock (tnth_nth a) /=. rewrite ltnS in Hi. rewrite -{3}[i]/(nat_of_ord (Ordinal Hi)). by rewrite -[x]/(tval (in_tuple x)) -tnth_nth -lock IH. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa)