(motive :
    (x : Type u_1) →
      (x_1 : CommRing x) →
        (x_2 : Type u_2) →
          (x_3 : AddCommGroup x_2) →
            (x_4 : Module x x_2) → (x_5 : List x) → RingTheory.Sequence.IsWeaklyRegular x_2 x_5 → Sort u_3) →
  (x : Type u_1) →
    (x_1 : CommRing x) →
      (x_2 : Type u_2) →
        (x_3 : AddCommGroup x_2) →
          (x_4 : Module x x_2) →
            (x_5 : List x) →
              (x_6 : RingTheory.Sequence.IsWeaklyRegular x_2 x_5) →
                ((R : Type u_1) →
                    (x : CommRing R) →
                      (M : Type u_2) →
                        (x_7 : AddCommGroup M) →
                          (x_8 : Module R M) →
                            (x_9 : RingTheory.Sequence.IsWeaklyRegular M []) → motive R x M x_7 x_8 [] x_9) →
                  ((α : Type u_1) →
                      (x : CommRing α) →
                        (M : Type u_2) →
                          (x_7 : AddCommGroup M) →
                            (x_8 : Module α M) →
                              (r : α) →
                                (rs : List α) →
                                  (h : RingTheory.Sequence.IsWeaklyRegular M (r :: rs)) →
                                    motive α x M x_7 x_8 (r :: rs) h) →
                    motive x x_1 x_2 x_3 x_4 x_5 x_6