Miscellaneous changes to the memory

* Remove generic path_typed instance for lists. For the zippers in the
  operational semantics, it goes the other way around.
* Remove constructor lemmas for values/memory_trees and use a generic tactic
  instead. This tactic uses the standard constructor tactic, but folds the
  type classes afterward.
Split load instruction, change redex splitting.

* Split the load instruction into two variants; one for arrays and the usual
  one. We have first class array values, so this is nicer.
* Use lists for the redex splitting of expressions, instead of an arbitrary
  finite set implementation. Lists are the best choice here because no
  duplicates are generated by construction.
Small stream library.
rename integers.v -> two_complement.v
Changes in preparation of the C type system and C front-end language

Major changes:
* Make void a base type, and include a proper void base value. This is necessary
  because expressions (free, functions without return value) can yield a void.
  We now also allow void casts conforming to the C standard.
* Various missing lemmas about typing, weakening, decidability, ...
* The operations "free" and "alloc" now operate on l-values instead of r-values.
  This removes some duplication.
* Improve notations of expressions and statements. Change the presence of the
  operators conforming to the C standard.

Small changes:
* Use the classes "Typed" and "TypeCheck" for validity of indexes in memory.
  This gives more uniform notations.
* New tactic "typed_inversion" performs inversion on an inductive predicate
  of type "Typed" and folds the premises.
* Remove a horrible hack in the definitions of the classes "FMap", "MBind",
  "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have
  defined a tactic "csimpl" that folds the results after performing an
  ordinary "simpl".
* Fast operation to remove duplicates from lists using hashsets.
* Make various type constructors (mainly finite map implementations) universe
  polymorphic by packing them into an inductive. This way, the whole C syntax
  can live in type, avoiding the need for (slow) universe checks.
A type system for expressions/statements/states and the type
preservation lemma.
Restore expression evaluation of constant expressions from the
master branch.
A front-end C language that is closer to C.

This language does not include explicit typing and r-to-l-value and
l-to-r-value conversions. Instead, these are infered, and we prove that
the resulting program is well-typed.
Glue together all the parts of the interpreter.