∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A}
  {p : (x : A) → x ∈ StarAlgebra.adjoin R s → Prop},
  (∀ (x : A) (h : x ∈ s), p x ⋯) →
    (∀ (r : R), p ((algebraMap R A) r) ⋯) →
      (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
            p x hx → p y hy → p (x * y) ⋯) →
          (∀ (x : A) (hx : x ∈ StarAlgebra.adjoin R s), p x hx → p (star x) ⋯) →
            ∀ {a : A} (ha : a ∈ StarAlgebra.adjoin R s), p a ha