This closes issue #25.

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

- Rename `gmap.to_gmap` into `gset_to_gmap`.
- Rename `gmap.of_gset` into `gset_to_propset`.
- Rename `coPset.to_Pset` into `coPset_to_Pset`.
- Rename `coPset.of_Pset` into `coPset_to_gset`.
- Rename `coPset.to_gset` into `coPset_to_gset`.
- Rename `coPset.of_gset` into `gset_to_coPset`.

The following `sed` script can be used for the first rename:

```
sed -i 's/to\_gmap/gset\_to\_gmap/g' $(find ./theories -name \*.v)
```

The latter is context sensitive, so was done manually.

Get rid of using `Collection` and favor `set` everywhere. Also, prefer conversion
functions that are called `X_to_Y`.

The following sed script performs most of the renaming, with the exception of:

- `set`, which has been renamed into `propset`. I couldn't do this rename
  using `sed` since it's too context sensitive.
- There was a spurious rename of `Vec.of_list`, which I correctly manually.
- Updating some section names and comments.

```
sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
' -i $(find -name "*.v")
```

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None  m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None  m !! j = None.

That is, we have to specify the type of `m`.

See also Coq bug #5712.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

(These instances are not defined for any FinMap to avoid overlapping
instances for EqDecision, which may have awkward consequences for
type class search).

This happened for example in <[i:=x]>∅, where simpl unfold insert (despite
it being declared simpl never) because ∅ reduces to a constructor.

This reverts commit 20b4ae55bdf00edb751ccdab3eb876cb9b13c99f, which does
not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).

This makes type checking more directed, and somewhat more predictable.

On the downside, it makes it impossible to declare the singleton on
lists as an instance of SingletonM and the insert and alter operations
on functions as instances of Alter and Insert. However, these were not
used often anyway.

Similar files (gmap, listset, ...) were already in singular form and
matched the name of the set/map data type.

simplify_equality        => simplify_eq
simplify_equality'       => simplify_eq/=
simplify_map_equality    => simplify_map_eq
simplify_map_equality'   => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality   => simplify_list_eq
f_equal'                 => f_equal/=

The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Also, make our redefinition of done more robust under different
orders of Importing modules.

Also do some minor clean up.