generalize hb : (𝚷 : Polarity) = Γ
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∀' p = r
⊢ Hierarchy 𝚷 s r → Hierarchy 𝚷 s p
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
p : Semiformula L μ (n + 1)
r : Semiformula L μ n
hr : ∀' p = r
Γ : Polarity
hb : 𝚷 = Γ
⊢ Hierarchy Γ s r → Hierarchy Γ s p