Theorem: LO.FirstOrder.Semiformula.Operator.LT.lt_inj (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
ξ₂ : Type u_1
n₂ : ℕ
inst✝ : L.LT
t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂
⊢ op(<).operator ![t₁, u₁] = op(<).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
Tactic:
simp [operator, LT.sentence_eq, Matrix.fun_eq_vec₂]
State after:
no goals