exact ih this
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
no goals