simp[DeltaZero, pi_zero_iff_sigma_zero]
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ DeltaZero p
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ Hierarchy 𝚺 0 p