rcases hq
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q✝ : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
q : Semiformula L μ₂ x✝
h : DeltaZero q
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
hq : ω.hom p = q
⊢ StrictHierarchy Γ✝ s✝ p
case refl
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ s✝ : ℕ
Γ✝ : Polarity
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ x✝
h : DeltaZero (ω.hom p)
⊢ StrictHierarchy Γ✝ s✝ p