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.
Edited by Robbert Krebbers
As remarked by @swasey this may be useful.
We currently have plenty of sets with a top element: propset, coPset, and soon cogset.