clear h1
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
⊢ M.toAbstract.eval s' []
case nil.mp
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s s' : σ
h2 : M.toAbstract.EpsilonClosure s' s
h3 : s ∈ M.accepting_state_list
⊢ M.toAbstract.eval s' []