intro hp hq
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
ihp : p✝.Open → Hierarchy Γ s p✝
ihq : q✝.Open → Hierarchy Γ s q✝
hp : p✝.Open
hq : q✝.Open
⊢ Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝