exact .εStep h₁ h (eq ▸ step)
case εStep
i j : ℕ
nfa nfa' : NFA
start : ℕ
h : i < nfa'.nodes.size
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j []
no goals