rcases 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)
h : Hierarchy b s (∀' p)
⊢ Hierarchy b s p
case ball
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ → !p✝)”)

case all
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚷 (s✝ + 1) p

case pi
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚺 s✝ p
⊢ Hierarchy 𝚷 (s✝ + 1) p

case dummy_sigma
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
p : Semiformula L ξ (n✝ + 1)
n s✝ : ℕ
a✝ : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p