constructor
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) ↔ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) → ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T) → ∃ M a x, M ⊧ₘ* T