induction' d with s ih
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
d : ℕ
⊢ Hierarchy Γ' (s + d + 1) p
case zero
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ Hierarchy Γ' (s + 0 + 1) p

case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s✝ : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s✝ p
Γ' : Polarity
s' : ℕ
h : s✝ < s'
s : ℕ
ih : Hierarchy Γ' (s✝ + s + 1) p
⊢ Hierarchy Γ' (s✝ + (s + 1) + 1) p