obtain ⟨i, _, _, _, path, step⟩ := path
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathToNext (↑next) nfa.nodes.size
    (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) cs
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ Expr.matches cs (Expr.char c)
case intro.intro.intro.intro.intro
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
i : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path :
  (↑(nfa.pushNode (Node.char c ↑next) ⋯)).pathIn nfa.nodes.size (↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start) i w✝¹
step : (↑(nfa.pushNode (Node.char c ↑next) ⋯)).stepIn nfa.nodes.size i (↑next) w✝
⊢ Expr.matches cs (Expr.char c)