have prev := ih (i := j') path
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
⊢ nfa.reaches i (m ++ [c])
case ind
nfa : NFA
m : List Char
c : Char
ih : ∀ {i : Fin nfa.nodes.size}, nfa.pathIn 0 (↑nfa.start) (↑i) m → nfa.reaches i m
i : Fin nfa.nodes.size
h : nfa.pathIn 0 (↑nfa.start) (↑i) (m ++ [c])
j k : ℕ
path : nfa.pathIn 0 (↑nfa.start) j m
step : k ∈ nfa.charStep j c
cls : ↑i ∈ nfa.εClosure k
j' : Fin nfa.nodes.size := ⟨j, ⋯⟩
prev : nfa.reaches j' m
⊢ nfa.reaches i (m ++ [c])