simp at hz ⊢
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : s✝ + 1 = 0 → Hierarchy 𝚺.alt (s✝ + 1) p✝
hz : s✝ + 1 + 1 = 0
⊢ Hierarchy 𝚷.alt (s✝ + 1 + 1) (∃' p✝)
no goals