have : nfa.pathIn 0 nfa.start i cs := pathIn_of_reaches h₁
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
⊢ Data.Expr.matches cs r
r : Data.Expr
nfa : NFA
i : Fin nfa.nodes.size
cs : List Char
eq : compile r = nfa
h₁ : nfa.reaches i cs
h₂ : nfa[i] = Node.done
hi : ↑i = 0
this : nfa.pathIn 0 (↑nfa.start) (↑i) cs
⊢ Data.Expr.matches cs r