cases p
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
case delta.mkDelta
L : Language
inst✝ : L.ORing
ξ✝ : Type v
n : ℕ
ξ : Type u_1
Γ : SigmaPiDelta
m✝ : ℕ
Γ' : Polarity
m : ℕ
a✝¹ : HSemiformula L ξ n (𝚺, 0)
a✝ : HSemiformula L ξ n (𝚷, 0)
⊢ Hierarchy Γ' m (a✝¹.mkDelta a✝).val