Add a type cogset A of finite/cofinite sets of elements of countable type A. When 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".