∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {motive : (a a_1 : FreeAlgebra R M) → TensorAlgebra.Rel R M a a_1 → Prop} {a a_1 : FreeAlgebra R M}
  (t : TensorAlgebra.Rel R M a a_1),
  (∀ {a b : M}, motive (FreeAlgebra.ι R (a + b)) (FreeAlgebra.ι R a + FreeAlgebra.ι R b) ⋯) →
    (∀ {r : R} {a : M}, motive (FreeAlgebra.ι R (r • a)) ((algebraMap R (FreeAlgebra R M)) r * FreeAlgebra.ι R a) ⋯) →
      motive a a_1 t