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₂⟩
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
case ind
nfa : NFA
i l : ℕ
cs : List Char
c✝ : Char
start : ℕ
path : nfa.pathIn start i l (cs ++ [c✝])
cs₁ cs₂ : List Char
c : Char
cs₃ : List Char
c' : Char
h : cs₁ ++ [c] = cs₂ ++ (cs₃ ++ [c'])
a✝ : cs₃ ++ [c'] = cs₃ → cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]
this : c = c' ∧ cs₁ = cs₂ ++ cs₃
⊢ cs₂ = cs₁ ++ [c] ∧ cs₃ ++ [c'] = [] ∨ ∃ cs₃', cs₁ = cs₂ ++ cs₃' ∧ cs₃ ++ [c'] = cs₃' ++ [c]