∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (motive : (∃ s, s.card = n ∧ LinearIndepOn R id ↑s) → Prop) (x : ∃ s, s.card = n ∧ LinearIndepOn R id ↑s),
  (∀ (s : Finset M) (s_card : s.card = n) (s_ind : LinearIndepOn R id ↑s), motive ⋯) → motive x