Add a type
cogset A of finite/cofinite sets of elements of countable type
A is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finite set.
The file includes efficient conversions to and from
gset A (for finite cogsets) and to
coPset (for arbitrary cogsets), as well as less efficient conversions to and from other finite sets and other sets with a top element.
Two things are marked TODO in the source, which really means "to discuss".