exact ⟨i₂, pcs₁ ++ (scs₁ ++ pcs₂), scs₂, by simp [eqs₁, eqs₂], path₁.trans (.step step₁ path₂), step₂⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ nfa.pathToNext k start i (cs ++ cs')
no goals