all_goals
  simp
  intro s a1 a2
  apply Exists.intro s
  tauto
case h.a.mp
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) →
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates
no goals