better use of "singleton" name

[ShapeOfMatter]

rename the existing thing singleton thing to something else.
define a new singleton = (@@ nobody), and use it in examples wherever it will improve readability.

[ShapeOfMatter]

Counterpoint: singleton p is no shorter than p @@ nobody, and the only sense I can think of in which it's more readable is that using singleton as Member p ps -> Subset '[p] ps would fit the "subset relations are like cons-lists" analogy better.
But my impression is that in the context of cons-lists, singleton is pretty rarely used, whereas whatever we use for Member p (p ': '[]) is apparently going to get used rather a lot in user-code, just judging by the examples dir.