simp only [← a2]
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.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
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list