case sigma ih =>
  rcases eq with ⟨p, rfl, rfl⟩
  exact (ih rfl).sigma
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
a✝ : Hierarchy 𝚷 s✝ p✝
ih : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy 𝚷 s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∃' p'
⊢ Hierarchy 𝚺 (s✝ + 1) p
no goals