simp [eqv, Semiformula.Operator.val]
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ eqv L a b
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ (Eval struc ![⟦a⟧, ⟦b⟧] Empty.elim) op(=).sentence ↔ (Eval inst✝ ![a, b] Empty.elim) op(=).sentence