Theorem: LO.FirstOrder.Semiterm.oringEmb_one (Logic/FirstOrder/Arith/Basic.lean)

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
⊢ lMap Language.oringEmb (Operator.const op(1)) = Operator.const op(1)
Tactic:
simp [Operator.const, lMap_func, Operator.operator, Operator.One.term_eq, Matrix.empty_eq]
State after:
no goals