cases step with
| charStep h₁ h₂ step => exact .charStep le h₂ step
| εStep h₁ h₂ step => exact .εStep le h₂ step
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ i
step : nfa.stepIn start i j cs
⊢ nfa.stepIn start' i j cs
no goals