exact ih this
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
no goals