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).