∀ {R : Type u_1} [inst : CommRing R] {P : Type u_2} [inst_1 : AddCommGroup P] [inst_2 : Module R P]
  (motive : (∃ n K x, K.FG) → Prop) (x : ∃ n K x, K.FG),
  (∀ (w : ℕ) (K : Submodule R (Fin w → R)) (ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K) (hK : K.FG), motive ⋯) → motive x