simp [operator, LE.sentence_eq, Eq.sentence_eq, LT.sentence_eq, Matrix.fun_eq_vec₂]
L : Language
ξ₂ : Type u_1
n₂ : ℕ
inst✝¹ : L.Eq
inst✝ : L.LT
t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂
⊢ op(≤).operator ![t₁, u₁] = op(≤).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
no goals