Theorem: LO.FirstOrder.Semiterm.val_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
v : Fin 0 → Semiterm L ξ✝ n✝
o : Const L
⊢ val s e ε (Operator.operator o v) = Operator.val o ![]
Tactic:
simp [val_operator, Matrix.empty_eq]
State after:
no goals