simpa
L : Language
inst✝ : L.LT
μ : Type v
n s : ℕ
Γ : Polarity
hb : 𝚷 = Γ
p✝ : Semiformula L μ (n + 1)
t✝ : Semiterm L μ (n + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy Γ s p✝
⊢ Hierarchy Γ s (“(#0 < !!t✝ → !p✝)”)
no goals