constructor
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p0 q0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := p0, symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
        q0 ∈ stop_state_list) →
    ∃ stop_state_list,
      (∃ a ∈ M_1.symbol_arrow_list,
          a.start_state = p0 ∧ a.symbol = c ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
        Sum.inr q0 ∈ stop_state_list