∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y : L),
  UniversalEnvelopingAlgebra.Rel R L ((TensorAlgebra.ι R) ⁅x, y⁆ + (TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x)
    ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)