induction path generalizing cs with
| base _ => simp at h
| @step i j k cs₁ cs₂ step rest ih =>
  match snoc_eq_append h with
  | .inl ⟨h₁, h₂⟩ =>
    simp [h₁, h₂] at step rest
    have := step.nil_of_snoc
    simp [this] at *
    cases step with
    | charStep le _ step =>
      exact ⟨i, .base le, j, charStep_of_charStep step, εClosure_of_pathIn rest⟩
  | .inr ⟨cs₂', h₁, h₂⟩ =>
    have ⟨j', k', path', step', cls⟩ := ih h₂.symm
    exact ⟨j', k', h₁ ▸ .step step path', step', cls⟩
nfa : NFA
i l : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h : cs ++ [c] = cs'
path : nfa.pathIn start i l cs'
⊢ ∃ j k, nfa.pathIn start i j cs ∧ k ∈ nfa.charStep j c ∧ l ∈ nfa.εClosure k
no goals