Define a TC for sets with a top element

As remarked by @swasey this may be useful.

We currently have plenty of sets with a top element: propset, coPset, and soon cogset.

mentioned in merge request !108 (merged)

Also, we can have a generic SetUnfoldElemOf for ⊤, instead of adhoc instances like https://gitlab.mpi-sws.org/iris/stdpp/blob/master/theories/propset.v#L53

changed the description

Reminder: on adding this TC, adjust lemmas like elem_of_cogset_to_set.

mentioned in commit 9a6de823

mentioned in merge request !111 (merged)

mentioned in commit e09f7ce3

closed via merge request !111 (merged)

mentioned in commit af368a15