case bex => simpa
L✝ : Language
inst✝¹ : L✝.LT
μ : Type v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n✝ : ℕ
b : Polarity
s n : ℕ
p✝ : Semiformula L ξ (n✝ + 1)
t✝ : Semiterm L ξ (n✝ + 1)
a✝¹ : t✝.Positive
a✝ : Hierarchy b s p✝
⊢ Hierarchy b s (“(#0 < !!t✝ ∧ !p✝)”)
no goals