simp only [NA.toDA]
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
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∈
      {S | ∃ s ∈ S, s ∈ N.acceptingStates} ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates