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

The rationale is that, just like the always lemmas about uPred and the frame-preserving updates for maps and iprdos, the versions with the ' are the "more specific" versions, hard-coding more assumptions in the shape of their conclusion.

Also do some minor clean up.

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.

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.

add basic notions of literals, unary operators and binary operators, and use them to define +, -, <=, ...

Actual proofs will end up using own and inv, and none of the notions defined in ownership.v

We should not depend on unreleased, git-only versions.
This reverts commit ee948028.

Remarks:
* eauto needs more fuel to automatically solve the side-conditions.
* ssreflect rewrite works if we do a set (φ ..) first. No idea why.

...unfortunately, that proof actually got longer because some automation no longer works

Notable changes:
* I am now using the same names for the fields of the language record and the
  instances in heap_lang. In order to deal with shadowing, I have put all
  definitions in heap_lang.v in a module.
* Instead of defining evaluation contexts recursively, these are now defined
  using lists. This way we can easily reuse operations on lists. For example,
  composition of evaluation contexts is just appending lists. Also, it allowed
  me to simplify the rather complicated proof of step_by_val as induction on
  the shape of contexts no longer results in a blow-up of the number of cases.
* Use better automation to prove all lemmas of heap_lang.
* I have introduced tactics to invert steps and to do steps. These tactics
  greatly helped simplifying boring parts of lifting lemmas.