feat: coPsets and namespaces

[Remyjck]

This PR is ready for review.

It corresponds to ports of Rocq's positive and stdpp's coPset and namespace.

These ports are not total (in particular, lacking automation to solve masking goals),
but there should already be enough here for most definitions relying on namespaces.

[markusdemedeiros]

This is great! Do you think there is a general interface for namespaces (downwards-closed sets or something) that this could be an instance of?

[Remyjck]

I guess they're downwards-closed sets where the dot .@ operator is some structure-preserving extending operation?

I'm not quite sure what the canonical interface for this would be (especially with regards to .@).

[lzy0505]

This PR has been waiting for reviews for a while and is essential for porting the fancy updates and invariants.
@markusdemedeiros I think I vaguely recalled you mentioning this was on your plan?

[markusdemedeiros]

I think it's mostly fine--just needs the build fixed and a bit of refactoring for cleanliness (non-terminal simps, combining rw's, etc.). @lzy0505 If you need this soon maybe you can refactor it?