simp [Operator.operator, Operator.LE.sentence_eq, Operator.Eq.sentence_eq, Operator.LT.sentence_eq]
L✝ : Language
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (op(≤).operator ![t, u]).Open
no goals