∀
  (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)
  (R : Type u_1) (x : CommRing R) (M : Type u_2) (x_1 : AddCommGroup M) (x_2 : Module R M)
  (x_3 : RingTheory.Sequence.IsWeaklyRegular M [])
  (h_1 :
    (R : Type u_1) →
      (x : CommRing R) →
        (M : Type u_2) →
          (x_4 : AddCommGroup M) →
            (x_5 : Module R M) → (x_6 : RingTheory.Sequence.IsWeaklyRegular M []) → motive R x M x_4 x_5 [] x_6)
  (h_2 :
    (α : Type u_1) →
      (x : CommRing α) →
        (M : Type u_2) →
          (x_4 : AddCommGroup M) →
            (x_5 : Module α M) →
              (r : α) →
                (rs : List α) →
                  (h : RingTheory.Sequence.IsWeaklyRegular M (r :: rs)) → motive α x M x_4 x_5 (r :: rs) h),
  (match R, x, M, x_1, x_2, [], x_3 with
    | R, x, M, x_4, x_5, [], x_6 => h_1 R x M x_4 x_5 x_6
    | α, x, M, x_4, x_5, r :: rs, h => h_2 α x M x_4 x_5 r rs h) =
    h_1 R x M x_1 x_2 x_3