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⟩
case step
nfa : NFA
i✝ l : ℕ
c : Char
start : ℕ
cs' : List Char
i j k : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
rest : nfa.pathIn start j k cs₂
ih :
  ∀ {cs : List Char},
    cs ++ [c] = cs₂ → ∃ j_1 k_1, nfa.pathIn start j j_1 cs ∧ k_1 ∈ nfa.charStep j_1 c ∧ k ∈ nfa.εClosure k_1
cs : List Char
h : cs ++ [c] = cs₁ ++ cs₂
⊢ ∃ j k_1, nfa.pathIn start i j cs ∧ k_1 ∈ nfa.charStep j c ∧ k ∈ nfa.εClosure k_1
no goals