simpa[val_func, ←Matrix.fun_eq_vec₂] using
  Structure.Add.add (L := L) (v 0) (v 1)
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Add
inst✝¹ : Add M
inst✝ : Structure.Add L M
v : Fin 2 → M
⊢ func Language.Add.add v = v 0 + v 1
no goals