∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (motive : (∃ n f, Function.Surjective ⇑f) → Prop) (x : ∃ n f, Function.Surjective ⇑f),
  (∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (hf : Function.Surjective ⇑f), motive ⋯) → motive x