{E : Type u_1} →
  [inst : SeminormedAddCommGroup E] →
    [inst_1 : StarAddMonoid E] →
      {motive : NormedStarGroup E → Sort u} →
        ((norm_star_le : ∀ (x : E), ‖star x‖ ≤ ‖x‖) → motive ⋯) → (t : NormedStarGroup E) → motive t