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

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