simp [models_def] at this
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
this : M ⊧ₘ (“∀' #0 = #0”)
⊢ eqv L a a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a : M
this : ∀ (x : M), op(=).val ![x, x]
⊢ eqv L a a