Countable types #
In this file we define a typeclass saying that a given
Sort* is countable. See also
for a version that singles out a specific encoding of elements of
α by natural numbers.
This file also provides a few instances of this typeclass. More instances can be found in other files.