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