simp at this
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c] ++ [])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
case snoc
nfa : NFA
i✝ : Fin nfa.nodes.size
m✝ : List Char
i : Fin nfa.nodes.size
j : ℕ
k : Fin nfa.nodes.size
c : Char
m : List Char
prev✝ : nfa.reaches i m
cls : ↑k ∈ nfa.εClosure j
ih : nfa.pathIn 0 (↑nfa.start) (↑i) m
step : j ∈ nfa[↑i].charStep c
ih' : nfa.pathIn 0 (↑nfa.start) j (m ++ [c])
this : nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])
⊢ nfa.pathIn 0 (↑nfa.start) (↑k) (m ++ [c])