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.

This way we can more easily state lemmas for concrete languages for
arbitrary global functors.

This enables us to remove a whole bunch of type annotations.

Instead, we have just a construction to create a CMRA from a RA. This
construction is also slightly generalized, it now works for RAs over any
timeless COFE instead of just the discrete COFE.

Also:
* Put tactics and big_ops for CMRAs in a separate file.
* Valid is now a derived notion (as the limit of validN), so it does not have
  to be defined by hand for each CMRA.

Todo:
Make the constructions DRA -> CMRA and RA -> CMRA more uniform.

copy the first half of the Iris appendix into the repository, so that we can keep the documentation in sync