Provide an Infinite typeclass and a generic implementation of Fresh.

This provides a generic implementation of Fresh for infinite types.

In detail, it adds:

• An Infinite type class. A type T is infinite if there is an injection from nat to T.
• A generic implementation of Fresh A C for an infinite type A and a finite collection type C, by way of linear search for a fresh element.
• Instances of Infinite for a handful of types, including positive/natural/integer types and string.
• A generic Fresh for finite collections of strings. As an implementation detail, the generated strings are all of the form "~n" for some natural number n.
• Some minor additions (pretty-printer for nat, Fix unfolding lemma for setoids).