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

State before:
L : Language
inst✝ : L.ORing
⊢ (Semiformula.lMap oringEmb) op(=).sentence = op(=).sentence
Tactic:
simp [Semiformula.Operator.Eq.sentence_eq, Semiformula.lMap_rel, Matrix.empty_eq]
State after:
no goals