Theorem: LO.FirstOrder.le_eq (Logic/FirstOrder/Order/Le.lean)

State before:
L : Language
inst✝¹ : Operator.Eq L
inst✝ : Operator.LT L
μ : Type u_1
n : ℕ
t₁ t₂ : Semiterm L μ n
⊢ LT.le.operator ![t₁, t₂] = (“(!!t₁ = !!t₂ ∨ !!t₁ < !!t₂)”)
Tactic:
simp [Operator.operator, Operator.or, LT.le, ←Rew.hom_comp_app, ←Matrix.fun_eq_vec₂]
State after:
no goals