generalize hq : ω.hom p = q
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
⊢ StrictHierarchy Γ s (ω.hom p) → StrictHierarchy Γ s p
L : Language
inst✝ : L.LT
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n₂
q : Semiformula L μ₂ n₂
hq : ω.hom p = q
⊢ StrictHierarchy Γ s q → StrictHierarchy Γ s p