simp [toAbstract]
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔ e.toAbstract.epsilon b c
case a.h.e'_2.h.h.e'_2.h.e.h.e'_2.h.h.a
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
state a b c : σ
⊢ (∃ l, (b, l) ∈ epsilon_arrow_list_to_graph e.epsilon_arrow_list ∧ c ∈ l) ↔
    ∃ stop_state_list,
      { start_state := b, stop_state_list := stop_state_list } ∈ e.epsilon_arrow_list ∧ c ∈ stop_state_list