∀ {R : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ιι : Type u_1}
  {ι : ιι → Type u_4}
  (motive :
    (GradedMonoid fun ii => PiTensorProduct R fun x => M) →
      (GradedMonoid fun ii => PiTensorProduct R fun x => M) → Prop)
  (x x_1 : GradedMonoid fun ii => PiTensorProduct R fun x => M),
  (∀ (ai : ιι) (a : PiTensorProduct R fun x => M) (bi : ιι) (b : PiTensorProduct R fun x => M),
      motive ⟨ai, a⟩ ⟨bi, b⟩) →
    motive x x_1