{𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] →
          [inst_3 : Module 𝕜 E] →
            {motive : SeminormedSpace.Core 𝕜 E → Sort u} →
              (t : SeminormedSpace.Core 𝕜 E) →
                ((norm_nonneg : ∀ (x : E), 0 ≤ ‖x‖) →
                    (norm_smul : ∀ (c : 𝕜) (x : E), ‖c • x‖ = ‖c‖ * ‖x‖) →
                      (norm_triangle : ∀ (x y : E), ‖x + y‖ ≤ ‖x‖ + ‖y‖) → motive ⋯) →
                  motive t