subst eqs
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
eqs : cs₂ = pcs ++ scs
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ (pcs ++ scs))