induction h with
| base => exact lt
| @step i j _ step _ ih =>
  have : j < nfa.nodes.size := by
    simp [εStep] at step
    split at step <;> exact lt_of_εStep step
  exact ih this
nfa : NFA
i j : ℕ
lt : i < nfa.nodes.size
h : j ∈ nfa.εClosure i
⊢ j < nfa.nodes.size
no goals