constructor
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p ↔ DeltaZero p
case mp
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p → DeltaZero p

case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ DeltaZero p → StrictHierarchy Γ 0 p