case hand ihp ihq => intro hp hq; exact ⟨ihp hp, ihq 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✝
no goals