rw [EpsilonNFA.eval_from_iff]
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list) ↔ e.toAbstract.accepts input
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.starting_state_list, e.toAbstract.eval s input) ↔ e.toAbstract.accepts input