rintro ⟨h⟩
case mp
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p → DeltaZero p
case mp.zero
L : Language
inst✝ : L.LT
μ : Type u_1
n✝ : ℕ
Γ : Polarity
p : Semiformula L μ n✝
n : ℕ
h : DeltaZero p
⊢ DeltaZero p