rcases hr with rfl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚷 = 𝚺
p✝ : Semiformula L μ (n + 1)
hp : Hierarchy 𝚷 (s✝ + 1) p✝
hr : p = p✝
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
s✝ : ℕ
hb : 𝚷 = 𝚺
hp : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p