rcases eq with ⟨p₁, 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✝ q✝ : Semiformula L μ₂ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
ihp : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = p✝ → Hierarchy Γ✝ s✝ p
ihq : ∀ {n₁ : ℕ} {ω : Rew L μ₁ n₁ μ₂ n✝} {p : Semiformula L μ₁ n₁}, ω.hom p = q✝ → Hierarchy Γ✝ s✝ p
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ n✝
p : Semiformula L μ₁ n₁
eq : ∃ p₁, ω.hom p₁ = p✝ ∧ ∃ x, ω.hom x = q✝ ∧ p = p₁ ⋎ x
⊢ Hierarchy Γ✝ s✝ p
case intro.intro.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✝
p₁ : Semiformula L μ₁ n₁
a✝¹ : Hierarchy Γ✝ s✝ (ω.hom p₁)
ihp : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₁ → Hierarchy Γ✝ s✝ p
p₂ : Semiformula L μ₁ n₁
a✝ : Hierarchy Γ✝ s✝ (ω.hom p₂)
ihq : ∀ {n₁_1 : ℕ} {ω_1 : Rew L μ₁ n₁_1 μ₂ n✝} {p : Semiformula L μ₁ n₁_1}, ω_1.hom p = ω.hom p₂ → Hierarchy Γ✝ s✝ p
⊢ Hierarchy Γ✝ s✝ (p₁ ⋎ p₂)