cases Γ
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ✝ : SigmaPiDelta
m✝ : ℕ
Γ : SigmaPiDelta
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (Γ, 0)
⊢ Hierarchy Γ' m p.val
case sigma
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.sigma, 0)
⊢ Hierarchy Γ' m p.val

case pi
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.pi, 0)
⊢ Hierarchy Γ' m p.val

case delta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
p : HSemiformula L ξ n (SigmaPiDelta.delta, 0)
⊢ Hierarchy Γ' m p.val