induction p using Semiformula.rec' <;> simp
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
⊢ p.Open → Hierarchy Γ s p
case hand
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : p✝.Open → Hierarchy Γ s p✝
a✝ : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝

case hor
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : p✝.Open → Hierarchy Γ s p✝
a✝ : q✝.Open → Hierarchy Γ s q✝
⊢ p✝.Open → q✝.Open → Hierarchy Γ s p✝ ∧ Hierarchy Γ s q✝