cases a2
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
case h.h.mp.intro
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
left✝ : p = 0 ∧ stop_state_list = [1]
right✝ : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1