∀ {R : Type u_1} [inst : Ring R]
  {motive : (M : Type u_2) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → IsFiniteLength R M → Prop}
  {M : Type u_2} {inst_1 : AddCommGroup M} {inst_2 : Module R M} (t : IsFiniteLength R M),
  (∀ (M : Type u_2) [inst_3 : AddCommGroup M] [inst_4 : Module R M] (t : IsFiniteLength R M),
      IsFiniteLength.below t → motive M t) →
    motive M t