cases step with
| charStep h₁ h₂ step =>
  exact .charStep h₁ h (eq ▸ step)
| εStep h₁ h₂ step =>
  exact .εStep h₁ h (eq ▸ step)
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
step : nfa.stepIn start i j cs
h : i < nfa'.nodes.size
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j cs
no goals