∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (a b : FreeNonUnitalNonAssocAlgebra R X),
  FreeLieAlgebra.Rel R X a b → (FreeLieAlgebra.liftAux R f) a = (FreeLieAlgebra.liftAux R f) b