Theorem: LO.FirstOrder.Arith.consistent_of_sound (Logic/FirstOrder/Arith/Basic.lean)

State before:
L : Language
inst✝¹ : Structure L ℕ
T : Theory L
F : Set (Sentence L)
inst✝ : SoundOn T F
hF : ⊥ ∈ F
b : T ⊢! ⊥
⊢ False
Tactic:
simpa using SoundOn.sound hF b
State after:
no goals