case _ a2_left a2_right =>
  cases a2_left
  case _ a2_left_left a2_left_right =>
    simp only [a2_left_right] at a2_right
    simp at a2_right
    tauto
α : 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
no goals