exact a2_right
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs
no goals