case dummy_sigma h => exact h.accum _
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
h : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
no goals