induction' n with n IH <;> simp [bexClosure, ←Rew.comp_app]
L : Language
inst✝ : L.LT
μ : Type v
ξ : Type u_1
b : Polarity
s n : ℕ
p : Semiformula L ξ n
v : Fin n → Semiterm L ξ 1
hv : ∀ (i : Fin n), (v i).Positive
⊢ Hierarchy b s (bexClosure (fun i => “#0 < !!(v i)”) p) ↔ Hierarchy b s p
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 (bexClosure (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
⊢ Hierarchy b s (bexClosure (fun x => “#0 < !!(v x.succ)”) (“(∃[#0 < !!([→ #0] (v 0))] !p)”)) ↔ Hierarchy b s p