funext p q
α : 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
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) = (p = 0 ∧ q = 1)