simp only [match_union_EpsilonNFA]
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (match_union_EpsilonNFA α σ_0 σ_1 M_0 M_1).toAbstract =
    match_union_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ {
        symbol_arrow_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).symbol_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).symbol_arrow_list,
        epsilon_arrow_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).epsilon_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).epsilon_arrow_list,
        starting_state_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list,
        accepting_state_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).accepting_state_list ++
            (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list }.toAbstract =
    match_union_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract