induction h2 with cases e
| accept _ h' => exact ⟨_, .refl, h'⟩
| eps _ _ _ _ h2 ih =>
  have ⟨s', h3, h4⟩ := ih rfl
  exact ⟨_, .head h2 h3, h4⟩
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
e : [] = l
h2 : M.toAbstract.eval s l
⊢ ∃ s', M.toAbstract.EpsilonClosure s s' ∧ s' ∈ M.accepting_state_list
no goals