simp only [EpsilonNFA.toAbstract]
α : Type
inst✝ : DecidableEq α
c : α
⊢ { symbol_arrow_list := [{ start_state := 0, symbol := c, stop_state_list := [1] }], epsilon_arrow_list := [],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_char_AbstractEpsilonNFA c
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_char_AbstractEpsilonNFA c