intro h
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
⊢ Hierarchy b s (∃' p) → Hierarchy b s p
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
b : Polarity
s : ℕ
p : Semiformula L ξ (n + 1)
h : Hierarchy b s (∃' p)
⊢ Hierarchy b s p