cases a2_left
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left : p = 0 ∧ stop_state_list = [1]
a2_right : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
case intro
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
left✝ : p = 0
right✝ : stop_state_list = [1]
⊢ p = 0 ∧ q = 1