simp [epsilon_closure_iff]
case nil
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
S : List σ
⊢ (∃ s ∈ M.epsilon_closure S, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s []
case nil
α σ : 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 []