intro xs x _ _ _ a4
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 → x_1.symbol = c → List.map Sum.inl x_1.stop_state_list = x → Sum.inr q0 ∉ x
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a✝² : x ∈ M_0.symbol_arrow_list
a✝¹ : x.start_state = p_0
a✝ : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q0 ∉ xs