cases a1
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
a1 :
  (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs) ∨
    ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
h✝ : ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
h✝ : ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs