Theorem: LO.FirstOrder.Arith.Hierarchy.exClosure (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
s n : ℕ
p : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 (s + 1) p
⊢ Hierarchy 𝚺 (s + 1) (∃* p)
Tactic:
simpa using exClosure (hp.ex)
State after:
no goals