∀ {R : Type u_2} {M : Type u_1} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M)
  (motive : Quotient.mk'' x ∈ Submodule.torsion R (M ⧸ Submodule.torsion R M) → Prop)
  (x_1 : Quotient.mk'' x ∈ Submodule.torsion R (M ⧸ Submodule.torsion R M)),
  (∀ (a : ↥(nonZeroDivisors R)) (hax : a • Quotient.mk'' x = 0), motive ⋯) → motive x_1