simp [LogicalConnective.ball, LogicalConnective.bex] at hr
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
r : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ : ∀ {p q : Semiformula L μ (n✝ + 1)}, p ⋏ q = p✝ → Hierarchy 𝚺 (s✝ + 1) p ∧ Hierarchy 𝚺 (s✝ + 1) q
p q : Semiformula L μ n✝
hr : p ⋏ q = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p ∧ Hierarchy 𝚷 (s✝ + 1 + 1) q
no goals