{E : Type u_8} →
  {motive : NormedAddCommGroup E → Sort u} →
    (t : NormedAddCommGroup E) →
      ([toNorm : Norm E] →
          [toAddCommGroup : AddCommGroup E] →
            [toMetricSpace : MetricSpace E] →
              (dist_eq : ∀ (x y : E), dist x y = ‖-x + y‖) →
                motive
                  { toNorm := toNorm, toAddCommGroup := toAddCommGroup, toMetricSpace := toMetricSpace,
                    dist_eq := dist_eq }) →
        motive t