unfold NFA.compile at eq
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
r : Data.Expr
nfa : NFA
cs : List Char
eq : ↑(done.pushRegex ⟨0, compile.proof_1⟩ r) = nfa
m : Data.Expr.matches cs r
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs