∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  {a a_1 : FreeNonUnitalNonAssocAlgebra R X} (t : FreeLieAlgebra.Rel R X a a_1),
  (∀ (a : FreeNonUnitalNonAssocAlgebra R X), motive (a * a) 0 ⋯) →
    (∀ (a b c : FreeNonUnitalNonAssocAlgebra R X), motive (a * (b * c)) (a * b * c + b * (a * c)) ⋯) →
      (∀ (t : R) {a b : FreeNonUnitalNonAssocAlgebra R X} (a_2 : FreeLieAlgebra.Rel R X a b),
          motive a b a_2 → motive (t • a) (t • b) ⋯) →
        (∀ {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X)
            (a_2 : FreeLieAlgebra.Rel R X a b), motive a b a_2 → motive (a + c) (b + c) ⋯) →
          (∀ (a : FreeNonUnitalNonAssocAlgebra R X) {b c : FreeNonUnitalNonAssocAlgebra R X}
              (a_2 : FreeLieAlgebra.Rel R X b c), motive b c a_2 → motive (a * b) (a * c) ⋯) →
            (∀ {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X)
                (a_2 : FreeLieAlgebra.Rel R X a b), motive a b a_2 → motive (a * c) (b * c) ⋯) →
              motive a a_1 t