assumption
case intro
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
q : Semiformula L μ n
Γ✝ : Polarity
s✝ n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
t : Semiterm L μ (n✝ + 1)
ht pt : t.Positive
hp : Hierarchy Γ✝ s✝ p
ih :
  ∀ {p_1 : Semiformula L μ (n✝ + 1 + 1)} {t : Semiterm L μ (n✝ + 1 + 1)},
    t.Positive → (“(∀[#0 < !!t] !p_1)”) = p → Hierarchy Γ✝ s✝ p_1
⊢ Hierarchy Γ✝ s✝ p
no goals