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

State before:
L : Language
T : Theory L
⊢ Semantics.Satisfiable (Struc L) T ↔ Satisfiable T
Tactic:
simp [satisfiable_iff_consistent'.{u, w}, satisfiable_iff_consistent]
State after:
no goals