intro hp
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
⊢ Hierarchy Γ s p → Hierarchy Γ s (“(∃[#0 < !!t] !p)”)
L : Language
inst✝ : L.LT
μ : Type v
Γ : Polarity
s n : ℕ
p : Semiformula L μ (n + 1)
t : Semiterm L μ (n + 1)
ht : t.Positive
hp : Hierarchy Γ s p
⊢ Hierarchy Γ s (“(∃[#0 < !!t] !p)”)