case ball p t pt hp ih =>
  rcases hq with ⟨rfl, rfl⟩
  assumption
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pt : t✝.Positive
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 : t = t✝ ∧ p = p✝
⊢ Hierarchy Γ✝ s✝ p
no goals