∀ {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}
  {motive_1 :
    {M : Type u_2} →
      {inst_1 : AddCommGroup M} → {inst_2 : Module R M} → (t : IsFiniteLength R M) → IsFiniteLength.below t → Prop},
  (∀ {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Subsingleton M], motive_1 ⋯ ⋯) →
    (∀ {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M}
        [inst_3 : IsSimpleModule R (M ⧸ N)] (a : IsFiniteLength R ↥N) (ih : IsFiniteLength.below a)
        (a_ih : motive (↥N) a), motive_1 a ih → motive_1 ⋯ ⋯) →
      ∀ {M : Type u_2} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {t : IsFiniteLength R M}
        (t_1 : IsFiniteLength.below t), motive_1 t t_1