simp only [match_char_EpsilonNFA]
α : Type
inst✝ : DecidableEq α
c : α
⊢ (match_char_EpsilonNFA c).toAbstract = match_char_AbstractEpsilonNFA c
α : 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