Theorem: LO.FirstOrder.Semiterm.val_const (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
⊢ val s e ε (Operator.const o) = Operator.val o ![]
Tactic:
simp [Operator.const, val_operator, Matrix.empty_eq]
State after:
no goals