simp [Semiterm.bv_eq_empty_of_positive (hv 0)]
case succ
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
IH :
  ∀ {p : Semiformula L ξ n} {v : Fin n → Semiterm L ξ 1},
    (∀ (i : Fin n), (v i).Positive) → (Hierarchy b s (ballClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p)
p : Semiformula L ξ (n + 1)
v : Fin (n + 1) → Semiterm L ξ 1
hv : ∀ (i : Fin (n + 1)), (v i).Positive
⊢ ([→ #0] (v 0)).Positive
no goals