simpa [models_def, Semiformula.Evalf, eq_finZeroElim, Empty.eq_elim] using
  eval_mk (H := H) (e := finZeroElim) (ε := Empty.elim) (p := σ)
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 ⊧ₘ σ
no goals