simp [Semiformula.ballLTSucc]
L : Language
inst✝³ : L.LT
μ : Type v
inst✝² : L.Zero
inst✝¹ : L.One
inst✝ : L.Add
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ n
⊢ Hierarchy Γ s (Semiformula.ballLTSucc t p) ↔ Hierarchy Γ s p
no goals