simp only [EpsilonNFA.eval_one_no_eps]
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈ e.eval_one_no_eps starting_state_list symbol ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ stop_state ∈
      (List.map (fun state => symbol_arrow_list_to_fun e.symbol_arrow_list state symbol)
            starting_state_list).join.dedup ↔
    ∃ state ∈ starting_state_list, e.toAbstract.symbol state symbol stop_state