exact ⟨_, .refl, h'⟩
case accept.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
s : σ
l : List α
start_state✝ : σ
h' : M.toAbstract.accepting start_state✝
⊢ ∃ s', M.toAbstract.EpsilonClosure start_state✝ s' ∧ s' ∈ M.accepting_state_list
no goals