intro d
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
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