obtain ⟨s₁, s₂, h3, h4, h5⟩ :
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure s s₂ ∧
      M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as := by
  clear h1; generalize e : a::as = l at h2
  induction h2 with cases e
  | sym _ _ _ _ h1 h2 => exact ⟨_, _, .refl, h2, h1⟩
  | eps _ _ _ h1 h2 ih =>
    have ⟨s₁, s₂, h3, h4, h5⟩ := ih rfl
    exact ⟨_, _, .head h2 h3, h4, h5⟩
case cons.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
⊢ ∃ s,
    (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
      M.toAbstract.eval s as
case cons.mpr.intro.intro.intro.intro
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s (a :: as)
s₁ s₂ : σ
h3 : M.toAbstract.EpsilonClosure s s₂
h4 : M.toAbstract.symbol s₂ a s₁
h5 : M.toAbstract.eval s₁ as
⊢ ∃ s,
    (∃ state, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state state) ∧ M.toAbstract.symbol state a s) ∧
      M.toAbstract.eval s as