cases Γ
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
Γ : Polarity
⊢ Hierarchy Γ (s✝ + 1 + 1) (∀' p✝)
case sigma
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.sigma (s✝ + 1 + 1) (∀' p✝)

case pi
L : Language
inst✝ : L.LT
μ : Type v
n s✝ : ℕ
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚺 s✝ p✝
⊢ Hierarchy Polarity.pi (s✝ + 1 + 1) (∀' p✝)