Theorem: LO.FirstOrder.consequence_iff_add_eq (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝ : Semiformula.Operator.Eq L
T : Theory L
σ : Sentence L
M : Type v
x✝² : Nonempty M
x✝¹ : Structure L M
x✝ : Structure.Eq L M
⊢ M ⊧ₘ* T⁼ → M ⊧ₘ σ ↔ M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
simp
State after:
no goals