Coinduction works on some uncountable set, for example, streams (or infinite list) which are A^{nat}, where A is the type of the elements in the stream. It looks a bit like induction on finite list, but slightly different.