simpa only [Nat.add_succ, add_zero] using ih.accum _
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
no goals