match step.step with
| .inl ⟨_, step⟩ => exact lt_of_charStep step
| .inr step => exact lt_of_εStep step
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step : nfa.stepIn start i j cs
⊢ j < nfa.nodes.size
no goals