rcases eq with ⟨hp, ⟨u, rfl, s, hs, rfl⟩, p, rfl, rfl⟩
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
t✝ : Semiterm L μ₂ (n✝ + 1)
pos : t✝.Positive
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₁, (∃ x, ω.q x = t✝ ∧ p₁ = (“#0 < !!x”)) ∧ ∃ x, ω.q.hom x = p✝ ∧ p = ∀[p₁] x
⊢ Hierarchy Γ✝ s✝ p
case intro.intro.intro.intro.refl.intro.intro
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
Γ✝ : Polarity
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
u : Semiterm L μ₁ (n₁ + 1)
pos : (ω.q u).Positive
p : Semiformula L μ₁ (n₁ + 1)
a✝ : Hierarchy Γ✝ s✝ (ω.q.hom p)
ih :
  ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)} {p_1 : Semiformula L μ₁ n₁_1},
    ω_1.hom p_1 = ω.q.hom p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ (“(∀[#0 < !!u] !p)”)