obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
next : ℕ
nfa : NFA
start start' i : ℕ
cs : List Char
le : start' ≤ start
path : nfa.pathToNext next start i cs
⊢ nfa.pathToNext next start' i cs
case intro.intro.intro.intro.intro
next : ℕ
nfa : NFA
start start' i : ℕ
cs : List Char
le : start' ≤ start
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start' i cs