case pi s _ _ hp ih =>
  rcases hq with rfl
  exact (show Hierarchy 𝚺 s p from by simpa using hp).accum _
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s✝ n : ℕ
q : Semiformula L μ n
s n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
hp : Hierarchy 𝚺 s p✝
ih :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∀[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 s p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t → !p)”) = p✝
⊢ Hierarchy 𝚷 (s + 1) p
no goals