intro xs x a1 a2 a3
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list,
      x_1.start_state = p_0 → List.map (Sum.inr ∘ Sum.inr) x_1.stop_state_list = x → Sum.inr (Sum.inl q_0) ∉ x
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a1 : x ∈ M_1.epsilon_arrow_list
a2 : x.start_state = p_0
a3 : List.map (Sum.inr ∘ Sum.inr) x.stop_state_list = xs
⊢ Sum.inr (Sum.inl q_0) ∉ xs