simp [LogicalConnective.ball, LogicalConnective.bex] at hq
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(∃[#0 < !!t] !p)”) = ∃' p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p
case dummy_pi
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : Hierarchy 𝚺 (s✝ + 1) p✝
a_ih✝ :
  ∀ {p : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∃[#0 < !!t] !p)”) = p✝ → Hierarchy 𝚺 (s✝ + 1) p
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hq : (“(#0 < !!t ∧ !p)”) = p✝
⊢ Hierarchy 𝚷 (s✝ + 1 + 1) p