exact zero <| (Hierarchy.rew_iff (ω := ω)).mpr h
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
x✝ s✝ : ℕ
Γ✝ : Polarity
p✝ : Semiformula L μ₁ x✝
h : DeltaZero p✝
μ₂ : Type u_2
n₂ : ℕ
ω : Rew L μ₁ x✝ μ₂ n₂
⊢ StrictHierarchy Γ✝ s✝ (ω.hom p✝)
no goals