Theorem: LO.FirstOrder.Arith.Hierarchy.ballLT_iff (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ n
⊢ Hierarchy Γ s (Semiformula.ballLT t p) ↔ Hierarchy Γ s p
Tactic:
simp [Semiformula.ballLT]
State after:
no goals