∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (motive : (∃ k h₂ h₃, LinearMap.id = h₃ ∘ₗ h₂) → Prop) (x : ∃ k h₂ h₃, LinearMap.id = h₃ ∘ₗ h₂),
  (∀ (w : ℕ) (f : M →ₗ[R] Fin w →₀ R) (g : (Fin w →₀ R) →ₗ[R] M) (eq : LinearMap.id = g ∘ₗ f), motive ⋯) → motive x