exact pathToNext_of_compile_of_pathInAux eq this rfl path
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
this : 0 < ↑nfa.start
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
no goals