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

State before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ T ⊨[Struc L] σ ↔
    ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [inst_2 : Structure.Eq L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ σ
Tactic:
rw [consequence_iff_eq]
State after:
no goals