Overhaul of the `Infinite`

/`Fresh`

infrastructure.

- The class
`Infinite A`

is now defined as having a function`fresh : list A → A`

, that given a list`xs`

, gives an element`x ∉ xs`

. - For most types this
`fresh`

function has a sensible computable behavior, for example:- For numbers, it yields one added to the maximal element in
`xs`

. - For strings, it yields the first string representation of a number that is
not in
`xs`

.

- For numbers, it yields one added to the maximal element in
- For any type
`C`

of finite sets with elements of infinite type`A`

, we lift the fresh function to`C → A`

.

As a consequence:

- It is now possible to pick fresh elements from
*any*finite set and from*any*list with elements of an infinite type. Before it was only possible for specific finite sets, e.g.`gset`

,`pset`

, ... - It makes the code more uniform. There was a lot of overlap between having a
`Fresh`

and an`Infinite`

instance. This got unified.