simpa [show s + (s' - s.succ) + 1 = s' from by simpa [Nat.succ_add] using Nat.add_sub_of_le h] using this (s' - s.succ)
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
this : ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
⊢ Hierarchy Γ' s' p
no goals