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