rw [consequence_iff_eq]
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 ⊧ₘ σ
no goals