rcases hr with ⟨rfl, rfl⟩
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋎ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p q : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p
a_ih✝¹ : ∀ {p_1 q : Semiformula L μ n✝}, p_1 ⋎ q = p → Hierarchy Γ✝ s✝ p_1 ∧ Hierarchy Γ✝ s✝ q
a✝ : Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q_1 : Semiformula L μ n✝}, p ⋎ q_1 = q → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q_1
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q