induction path with
| base _ => exact assm
| @step i j _ _ _ step _ ih =>
  have : j < nfa.nodes.size := by
    cases step with
    | charStep _ _ step => exact lt_of_charStep step
    | εStep _ _ step => exact lt_of_εStep step
  exact ih this
cs : List Char
nfa : NFA
start i i' : ℕ
assm : i < nfa.nodes.size
path : nfa.pathIn start i i' cs
⊢ i' < nfa.nodes.size
no goals