simp [Operator.operator, eval_substs, Operator.val]
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ n
⊢ (Eval s e ε) (o.operator v) ↔ o.val fun i => Semiterm.val s e ε (v i)
no goals