simp [val_operator, Matrix.empty_eq]
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
v : Fin 0 → Semiterm L ξ✝ n✝
o : Const L
⊢ val s e ε (Operator.operator o v) = Operator.val o ![]
no goals