∀ {R : Type u_2} [inst : CommRing R] {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (motive : (∃ s, Nonempty (Module.Basis (↥s) R M)) → Prop) (x : ∃ s, Nonempty (Module.Basis (↥s) R M)),
  (∀ (w : Finset M) (b : Module.Basis (↥w) R M), motive ⋯) → motive x