rw[eq_comm] at hz
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : 0 = z
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
⊢ Hierarchy Γ z p → Hierarchy Γ.alt z p