simp only [NA.memAccepts]
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔ N.accepts cs
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates