obtain ⟨s', h3, h4⟩ : ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list := by
  clear h1; generalize e : [] = l at h2
  induction h2 with cases e
  | accept _ h' => exact ⟨_, .refl, h'⟩
  | eps _ _ _ _ h2 ih =>
    have ⟨s', h3, h4⟩ := ih rfl
    exact ⟨_, .head h2 h3, h4⟩
case nil.mpr
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
⊢ ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list
case nil.mpr.intro.intro
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
h1 : s ∈ S
h2 : M.toAbstract.eval s []
s' : σ
h3 : M.toAbstract.EpsilonClosure s s'
h4 : s' ∈ M.accepting_state_list
⊢ ∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list