Theorem: LO.FirstOrder.Structure.one_eq_of_lang (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.One
inst✝¹ : One M
inst✝ : Structure.One L M
⊢ func Language.One.one ![] = 1
Tactic:
simpa[Semiterm.Operator.val, Semiterm.Operator.One.one, val_func, ←Matrix.fun_eq_vec₂] using
  Structure.One.one (L := L) (M := M)
State after:
no goals