Theorem: LO.FirstOrder.Semiformula.Operator.Eq.equal_inj (Logic/FirstOrder/Basic/Operator.lean)

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