∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (motive :
    (∃ n ι x p,
        ∃ (_ : ∀ (i : ι), Irreducible (p i)),
          ∃ e, Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun i => R ⧸ R ∙ p i ^ e i)) →
      Prop)
  (x :
    ∃ n ι x p,
      ∃ (_ : ∀ (i : ι), Irreducible (p i)),
        ∃ e, Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun i => R ⧸ R ∙ p i ^ e i)),
  (∀ (m : ℕ) (ι : Type u_1) (w : Fintype ι) (p : ι → R) (irr : ∀ (i : ι), Irreducible (p i)) (n : ι → ℕ)
      (e : M ≃ₗ[R] (Fin m →₀ R) × DirectSum ι fun i => R ⧸ R ∙ p i ^ n i), motive ⋯) →
    motive x