induction path₁ with
| base _ => exact path₂
| step step _ ih =>
  simp
  exact .step step (ih path₂)
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start : ℕ
path₁ : nfa.pathIn start i j cs
path₂ : nfa.pathIn start j k cs'
⊢ nfa.pathIn start i k (cs ++ cs')
no goals