exact (ih _).accum _
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
n₁ : ℕ
μ₂ : Type u_2
Γ : Polarity
s : ℕ
p : Semiformula L μ₁ n₁
s✝ n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : ∀ {n₂ : ℕ} (ω : Rew L μ₁ (n✝ + 1) μ₂ n₂), Hierarchy 𝚷 s✝ (ω.hom p✝)
n₂ : ℕ
ω : Rew L μ₁ n✝ μ₂ n₂
⊢ Hierarchy 𝚺 (s✝ + 1) (ω.q.hom p✝)
no goals