Theorem: LO.FirstOrder.Structure.eq_lang (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type u_1
inst✝² : Structure L M
inst✝¹ : L.Eq
inst✝ : Structure.Eq L M
v : Fin 2 → M
⊢ rel Language.Eq.eq v ↔ v 0 = v 1
Tactic:
simpa[Semiformula.Operator.Eq.sentence_eq, eval_rel, ←Matrix.fun_eq_vec₂] using
  Structure.Eq.eq (L := L) (v 0) (v 1)
State after:
no goals