simp at a2_right
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q ∈ [1]
⊢ p = 0 ∧ q = 1
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q = 1
⊢ p = 0 ∧ q = 1