constructor
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) ↔
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list
case mp
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l) →
    ∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list

case mpr
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
starting_state_list : List σ
symbol : α
stop_state : σ
⊢ (∃ state ∈ starting_state_list,
      ∃ stop_state_list,
        { start_state := state, symbol := symbol, stop_state_list := stop_state_list } ∈ e.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) →
    ∃ a ∈ starting_state_list,
      ∃ l,
        (∃ a_1 ∈ e.symbol_arrow_list, (a_1.start_state = a ∧ a_1.symbol = symbol) ∧ a_1.stop_state_list = l) ∧
          stop_state ∈ l