constructor
case right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun state => state ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) = fun p =>
      match p with
      | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
      | x => False) ∧
    (fun state => state ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
      match p with
      | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
      | x => False
case right.right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inr (List.map Sum.inl M_0.starting_state_list)) = fun p =>
    match p with
    | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
    | x => False

case right.right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
    match p with
    | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
    | x => False