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