simp [Set.mem_def]
L✝ : Language
inst✝⁵ : L✝.LT
μ : Type v
L : Language
inst✝⁴ : (k : ℕ) → DecidableEq (L.Func k)
inst✝³ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝² : L.LT
inst✝¹ : Structure L ℕ
T : Theory L
inst✝ : SigmaOneSound T
⊢ ⊥ ∈ Hierarchy 𝚺 1
no goals