{E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    {motive : InnerProductSpaceable E → Sort u} →
      ((parallelogram_identity : ∀ (x y : E), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) →
          motive ⋯) →
        (t : InnerProductSpaceable E) → motive t