∀ {I : Type u} [inst : DecidableEq I] {R : Type v} [inst_1 : CommSemiring R] {A : I → Type w}
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)]
  {motive : (a a_1 : LinearAlgebra.FreeProduct.FreeTensorAlgebra R A) → LinearAlgebra.FreeProduct.rel R A a a_1 → Prop}
  {a a_1 : LinearAlgebra.FreeProduct.FreeTensorAlgebra R A} (t : LinearAlgebra.FreeProduct.rel R A a a_1),
  (∀ {i : I}, motive ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1 ⋯) →
    (∀ {i : I} {a₁ a₂ : A i},
        motive
          ((TensorAlgebra.tprod R (DirectSum I fun i => A i) 2) fun x =>
            match x with
            | 0 => (DirectSum.lof R I A i) a₁
            | 1 => (DirectSum.lof R I A i) a₂)
          ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) (a₁ * a₂))) ⋯) →
      motive a a_1 t