A set is countable if there exists an encoding of the set into the natural numbers.
An encoding is an injection with a partial inverse, which can be viewed as a
constructive analogue of countability. (For the most part, theorems about
countable will be classical and
encodable will be constructive.)
Enumerate elements in a countable set.