simp
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.symbol_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 →
        x_1.symbol = c →
          List.map Sum.inl x_1.stop_state_list = x →
            Sum.inl q_0 ∈ x →
              ∃ stop_state_list,
                { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
                  q_0 ∈ stop_state_list