induction H <;> try simp [LogicalConnective.ball, LogicalConnective.bex] at hr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p q r : Semiformula L μ n
hr : p ⋏ q = r
H : Hierarchy Γ s r
⊢ Hierarchy Γ s p ∧ Hierarchy Γ s q
case and
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ : Hierarchy Γ✝ s✝ p✝
a✝ : Hierarchy Γ✝ s✝ q✝
a_ih✝¹ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = p✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
a_ih✝ : ∀ {p q : Semiformula L μ n✝}, p ⋏ q = q✝ → Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q
p q : Semiformula L μ n✝
hr : p = p✝ ∧ q = q✝
⊢ Hierarchy Γ✝ s✝ p ∧ Hierarchy Γ✝ s✝ q