exact ((hp.accum 𝚺).accum 𝚺).ex
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s✝ + 1) p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1 + 1) (∃' p✝)
no goals