∀ {R : Type u_2} {A : Type u_1} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (p q : NonUnitalStarSubalgebra R A), ((fun {s} => s.carrier) = fun {s} => s.carrier) → p = q