This way we avoid many one-off indexes and no longer need special cases for
index 0 in many definitions. For example, the definition of the distance
relation on option and excl has become much easier. Also, uPreds no longer need
to hold at index 0.

In order to make this change possible, we had to change the notions of
"contractive functions" and "chains" slightly.

Thanks to Aleš Bizjak and Amin Timany for suggesting this change and to help
with the proofs.

Now notations are pretty printed in the same way as they are parsed.
Before "let x := e1 in e2" was notation for "(fun x => e2) e1",
resulting in overlapping notations for the same thing.

It is now slightly below implication. In order to do this, I had to change
the notation from P ={E1,E2}=> Q to P >{E1,E2}=> Q because the prefer ={n
is already used at level 70 for the distance of the metric.

We can use a named representation because we only substitute closed values. This
idea is borrowed from Pierce's Software Foundations.

The named representation has the following advantages:
* Programs are much better readable than those using De Bruijn indexes.
* Substitutions on closed terms (where all variables are explicit strings) can
  be performed by a mere simpl instead of Autosubst's asimpl. The performance
  of simpl seems better than asimpl.
* Syntactic sugar refolds better.