generalize hr : p ⋏ q = r
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s (p ⋏ q) → Hierarchy Γ s p ∧ Hierarchy Γ s q
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋏ q = r
⊢ Hierarchy Γ s r → Hierarchy Γ s p ∧ Hierarchy Γ s q