Theorem: LO.FirstOrder.Arith.consistent_of_sigmaOneSound (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
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
Tactic:
simp [Set.mem_def]
State after:
no goals