simpa[Semiterm.Operator.val, Semiterm.Operator.Zero.zero, val_func, ←Matrix.fun_eq_vec₂] using
  Structure.Zero.zero (L := L) (M := M)
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Zero
inst✝¹ : Zero M
inst✝ : Structure.Zero L M
⊢ func Language.Zero.zero ![] = 0
no goals