simp [eval_operator, Matrix.constant_eq_singleton]
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 1
t : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t]) ↔ o.val ![Semiterm.val s e ε t]
no goals