simp
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state ∈ stop_state_list) ∧ stop_state_list = [1]) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
no goals