Fixes new Coq master warning deprecated-hint-without-locality.

Code affected by a00d9bd8.

This was inconsistent and not explained before.

This follows iris!387
This closes issue #54.

The `Equiv` instance for the domain is not needed.

This is in preparation for coq/coq#9274.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

The notation was parsing-only and all it did was reorder the arguments for
from_option.  This creates just a needless divergence between what is written
and what is printed.  Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.

This followed from discussions in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134

This follows the associativity in Haskell. So, something like

  f <$> g <$> h

Is now parsed as:

  (f <$> g) <$> h

Since the functor is a generalized form of function application, this also now
also corresponds with the associativity of function application, which is also
left associative.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.

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

We typically use the _1 and _2 suffix to denote individual directions
of a lemmas that is a biimplication.

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.