∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : Module ℝ M] (Q : QuadraticForm ℝ M)
  (motive : (∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))) → Prop)
  (x : ∃ w, QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))),
  (∀ (w : Fin (Module.finrank ℝ M) → SignType)
      (hw : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))), motive ⋯) →
    motive x