∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  {motive_1 :
    {a a_1 : FreeNonUnitalNonAssocAlgebra R X} →
      (t : FreeLieAlgebra.Rel R X a a_1) → FreeLieAlgebra.Rel.below t → Prop},
  (∀ (a : FreeNonUnitalNonAssocAlgebra R X), motive_1 ⋯ ⋯) →
    (∀ (a b c : FreeNonUnitalNonAssocAlgebra R X), motive_1 ⋯ ⋯) →
      (∀ (t : R) {a b : FreeNonUnitalNonAssocAlgebra R X} (a_1 : FreeLieAlgebra.Rel R X a b)
          (ih : FreeLieAlgebra.Rel.below a_1) (a_ih : motive a b a_1), motive_1 a_1 ih → motive_1 ⋯ ⋯) →
        (∀ {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X)
            (a_1 : FreeLieAlgebra.Rel R X a b) (ih : FreeLieAlgebra.Rel.below a_1) (a_ih : motive a b a_1),
            motive_1 a_1 ih → motive_1 ⋯ ⋯) →
          (∀ (a : FreeNonUnitalNonAssocAlgebra R X) {b c : FreeNonUnitalNonAssocAlgebra R X}
              (a_1 : FreeLieAlgebra.Rel R X b c) (ih : FreeLieAlgebra.Rel.below a_1) (a_ih : motive b c a_1),
              motive_1 a_1 ih → motive_1 ⋯ ⋯) →
            (∀ {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X)
                (a_1 : FreeLieAlgebra.Rel R X a b) (ih : FreeLieAlgebra.Rel.below a_1) (a_ih : motive a b a_1),
                motive_1 a_1 ih → motive_1 ⋯ ⋯) →
              ∀ {a a_1 : FreeNonUnitalNonAssocAlgebra R X} {t : FreeLieAlgebra.Rel R X a a_1}
                (t_1 : FreeLieAlgebra.Rel.below t), motive_1 t t_1