simp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
⊢ (Sum.inr (Sum.inl p_0) ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) =
    match Sum.inr (Sum.inl p_0) with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False
no goals