∀ {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 y : A) → x ∈ StarAlgebra.adjoin R s → y ∈ StarAlgebra.adjoin R s → Prop},
  (∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯) →
      (∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯) →
        (∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯) →
          (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
              (hz : z ∈ StarAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
            (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
                (hz : z ∈ StarAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
              (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
                  (hz : z ∈ StarAlgebra.adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
                (∀ (x y z : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s)
                    (hz : z ∈ StarAlgebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                  (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
                      p x y hx hy → p (star x) y ⋯ hy) →
                    (∀ (x y : A) (hx : x ∈ StarAlgebra.adjoin R s) (hy : y ∈ StarAlgebra.adjoin R s),
                        p x y hx hy → p x (star y) hx ⋯) →
                      ∀ {a b : A} (ha : a ∈ StarAlgebra.adjoin R s) (hb : b ∈ StarAlgebra.adjoin R s), p a b ha hb