rw [←eq, compile]
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑nfa.start
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑(↑(done.pushRegex ⟨0, compile.proof_1⟩ r)).start