∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂}, (∀ (x : L₁), f x = g x) → f = g