∀ (R : Type u_2) [inst : Ring R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (motive :
    (∃ n D d x x_1,
        (∀ (i : Fin n), NeZero (d i)) ∧
          Nonempty (Module.End R M ≃ₐ[ℕ] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))) →
      Prop)
  (x :
    ∃ n D d x x_1,
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (Module.End R M ≃ₐ[ℕ] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))),
  (∀ (n : ℕ) (D : Fin n → Type u_1) (d : Fin n → ℕ) (w : (i : Fin n) → DivisionRing (D i))
      (w_1 : (i : Fin n) → Algebra ℕ (D i)) (hd : ∀ (i : Fin n), NeZero (d i))
      (e : Module.End R M ≃ₐ[ℕ] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)), motive ⋯) →
    motive x