∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M)
  (motive : (∃ s', ↑s' ⊆ s ∧ Submodule.span R s = Submodule.span R ↑s') → Prop)
  (h : ∃ s', ↑s' ⊆ s ∧ Submodule.span R s = Submodule.span R ↑s'),
  (∀ (s' : Finset M) (left : ↑s' ⊆ s) (h : Submodule.span R s = Submodule.span R ↑s'), motive ⋯) → motive h