Theorem: LO.FirstOrder.Arith.oringEmb_operator_add_val (Logic/FirstOrder/Arith/Model.lean)

State before:
L : Language
inst✝ : L.ORing
⊢ Semiterm.lMap oringEmb op(+).term = op(+).term
Tactic:
simp [Semiterm.Operator.Add.term_eq, Semiterm.lMap_func, Matrix.empty_eq]
State after:
no goals