simp only [NFA.mem_accepts]
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔ N.accepts cs
case h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
N : NFA α σ
cs : List α
⊢ N.to_DFA.eval_from N.to_DFA.starting_state cs ∈ N.to_DFA.accepting_state_list ↔
    ∃ s ∈ N.eval_from N.starting_state_list cs, s ∈ N.accepting_state_list