rcases hq with ⟨_, rfl, rfl⟩
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ : ℕ
p✝ : Semiformula L μ₂ (n✝ + 1)
h : StrictHierarchy 𝚺 s✝ p✝
ih : ∀ {n₁ : ℕ} {p : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ (n✝ + 1)), ω.hom p = p✝ → StrictHierarchy 𝚺 s✝ p
n₁ : ℕ
p : Semiformula L μ₁ n₁
ω : Rew L μ₁ n₁ μ₂ n✝
hq : ∃ p', ω.q.hom p' = p✝ ∧ p = ∀' p'
⊢ StrictHierarchy 𝚷 (s✝ + 1) p
case intro.intro
L : Language
inst✝ : L.LT
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
s✝ n✝ n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
w✝ : Semiformula L μ₁ (n₁ + 1)
h : StrictHierarchy 𝚺 s✝ (ω.q.hom w✝)
ih :
  ∀ {n₁_1 : ℕ} {p : Semiformula L μ₁ n₁_1} (ω_1 : Rew L μ₁ n₁_1 μ₂ (n✝ + 1)),
    ω_1.hom p = ω.q.hom w✝ → StrictHierarchy 𝚺 s✝ p
⊢ StrictHierarchy 𝚷 (s✝ + 1) (∀' w✝)