induction h <;> try simp at hz ⊢
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
hz : z = 0
h : Hierarchy Γ z p
⊢ Hierarchy Γ.alt z p
case and
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝

case or
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ q✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ p✝ ∧ Hierarchy Γ✝.alt s✝ q✝

case ball
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !p✝)”)

case bex
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
p : Semiformula L μ n
z : ℕ
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
a_ih✝ : s✝ = 0 → Hierarchy Γ✝.alt s✝ p✝
hz : s✝ = 0
⊢ Hierarchy Γ✝.alt s✝ (“(∃[#0 < !!t✝] !p✝)”)