{E : Type u_1} →
  [inst : SeminormedAddCommGroup E] →
    {motive : UniformConvexSpace E → Sort u} →
      (t : UniformConvexSpace E) →
        ((uniform_convex :
              ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ) →
            motive ⋯) →
          motive t