simp
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun x x x => False, epsilon := fun p q => p = 0 ∧ q = 1, start := fun p => p = 0,
      accepting := fun p => p = 1 }
α : Type
inst✝ : DecidableEq α
⊢ (fun start_state stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p q => p = 0 ∧ q = 1