intro ⟨s, ⟨s', h1, h2⟩, h3⟩
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s, (∃ start_state ∈ S, M.toAbstract.EpsilonClosure start_state s) ∧ s ∈ M.accepting_state_list) →
    ∃ s ∈ S, M.toAbstract.eval s []
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h1 : s' ∈ S
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ ∃ s ∈ S, M.toAbstract.eval s []