exact a2_right
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a3_left : x ∈ M_0.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
no goals