Setoids, setoids1, sets, and the like. The mess begins.

Setoids, setoids1, sets, and the like. The mess begins.

Note: the (partially) interesting part of the development is that canonical
structures (provided by unification hints) allow to perform setoid rewriting
by hieroglyphs without having to use "rich operators". On the other hand, after
the application what you get is always an enriched structure and thus either
it is normalized away or the theory becomes a mix of rich/unrich. The latter
phenomena happens anyway because, in algebraic structures, you need to put
things in rich structures to have all the properties you need.

algebra/magmas does not work because refinement of projection is too weak