Theorem: LO.FirstOrder.consequence_iff_consequence (Logic/FirstOrder/Completeness/Completeness.lean)

State before:
L : Language
T : Theory L
σ : Sentence L
⊢ T ⊨[Struc L] σ ↔ T ⊨ σ
Tactic:
simp [Semantics.consequence_iff_not_satisfiable, satidfiable_iff_satisfiable.{u, w}]
State after:
no goals