simp at hp
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
hp : Hierarchy 𝚷 (s✝ + 1) (“(#0 < !!t → !p)”)
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∀[#0 < !!t_1] !p_1)”) = (“(#0 < !!t → !p)”) → Hierarchy 𝚷 (s✝ + 1) p_1
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht : t.Positive
a_ih✝ :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t_1 : Semiterm L μ (n✝ + 1 + 1)},
    t_1.Positive → (“(∀[#0 < !!t_1] !p_1)”) = (“(#0 < !!t → !p)”) → Hierarchy 𝚷 (s✝ + 1) p_1
hp : Hierarchy 𝚷 (s✝ + 1) p
⊢ Hierarchy 𝚺 (s✝ + 1 + 1) p