exact a1
case mpr.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ q_0 ∈ xs
no goals