simp [lMap_func, Rew.func, Operator.operator, Operator.Add.term_eq, Matrix.empty_eq]
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ lMap Language.oringEmb (op(+).operator v) = (‘(!!(lMap Language.oringEmb (v 0)) + !!(lMap Language.oringEmb (v 1)))’)
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i