simp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inl arrow.start_state, stop_state_list := List.map Sum.inl arrow.stop_state_list })
              M_0.epsilon_arrow_list ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, stop_state_list := List.map Sum.inr arrow.stop_state_list })
              M_1.epsilon_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inl q_0) with
    | (Sum.inl p', Sum.inl q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | (Sum.inr p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q_0 ∈ stop_state_list