simp [Operator.operator, Operator.or, LT.le, ←Rew.hom_comp_app, ←Matrix.fun_eq_vec₂]
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₂)”)
no goals