exact ⟨i', pcs, scs, rfl, .step (.εStep h₁ h₂ step) path, step'⟩
case intro.intro.intro.intro.intro.εStep
nfa : NFA
i j next start i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathToNext next start i ([] ++ (pcs ++ scs))
no goals