cases cs₃ using List.list_reverse_induction with
| base =>
  simp at h
  exact .inl ⟨h.symm, rfl⟩
| ind cs₃ c' =>
  have : c = c' ∧ cs₁ = cs₂ ++ cs₃ := by
    have h₁ := congrArg List.reverse h
    simp at h₁
    have h₂ := congrArg List.reverse h₁.right
    simp at h₂
    exact ⟨h₁.left, h₂⟩
  simp [this]
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ cs₃ : List Char
c : Char
h : cs₁ ++ [c] = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ = cs₃' ++ [c]
no goals