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