Theorem: LO.FirstOrder.Structure.Eq.QuotEq.models_iff (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
σ : Sentence L
⊢ QuotEq H ⊧ₘ σ ↔ M ⊧ₘ σ
Tactic:
simpa [models_def, Semiformula.Evalf, eq_finZeroElim, Empty.eq_elim] using
  eval_mk (H := H) (e := finZeroElim) (ε := Empty.elim) (p := σ)
State after:
no goals