exact ball pos ih
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
t✝ : Semiterm L μ (n✝ + 1)
pos : t✝.Positive
a✝ : Hierarchy Γ✝ s✝ p✝
ih : Hierarchy Γ✝.alt s✝ (~p✝)
⊢ Hierarchy Γ✝.alt s✝ (“(∀[#0 < !!t✝] !(~p✝))”)
no goals