Theorem: LO.FirstOrder.Semiformula.eval_operator (Logic/FirstOrder/Basic/Operator.lean)

State before:
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)
Tactic:
simp [Operator.operator, eval_substs, Operator.val]
State after:
no goals