Theorem: LO.FirstOrder.Arith.Hierarchy.zero_iff (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ Γ' : Polarity
p : Semiformula L μ n
⊢ Hierarchy Γ 0 p ↔ Hierarchy Γ' 0 p
Tactic:
rcases Γ <;> rcases Γ' <;> simp[pi_zero_iff_sigma_zero]
State after:
no goals