simp [Operator.operator, val_substs]
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s e ε (o.operator v) = o.val fun x => val s e ε (v x)
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ✝ n✝
⊢ val s (fun x => val s e ε (v x)) (fun a => instIsEmptyEmpty.elim a) o.term = o.val fun x => val s e ε (v x)