rintro ⟨hp, hq⟩
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q → Hierarchy Γ s (p ⋎ q)
case intro
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q : Semiformula L μ n
hp : Hierarchy Γ s p
hq : Hierarchy Γ s q
⊢ Hierarchy Γ s (p ⋎ q)