{R : Type u} →
  [inst : AddMonoid R] →
    {motive : StarAddMonoid R → Sort u_1} →
      ([toInvolutiveStar : InvolutiveStar R] →
          (star_add : ∀ (r s : R), star (r + s) = star r + star s) →
            motive { toInvolutiveStar := toInvolutiveStar, star_add := star_add }) →
        (t : StarAddMonoid R) → motive t