∀ {M : Type u_1} [inst : Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u_2))
  (p : ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))) {j j' : CategoryTheory.SingleObj M},
  ↑p ∈ MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M))