Tidying up

  Moving definitions around so that they are in the right module.
  Mostly uninteresting.
Adding new tests

  Multiplication is iterated addition ;
  Exponentiation is iterated multiplication ;
  The `Norm` test cases focus on partial evaluation whilst the
  `Numbers` ones are closed computations.
Defining an eta-free model

  Following the intuition detailled in this blog post:
  http://blog.gallais.org/read/glueing-terms-model
  we define a model with more structure in order not to have to
  internalize eta. This should be more efficient as we are not
  generating useless closures...

  Eta can be recovered when testing conversion with a mechanism
  à la Coq where it is performed lazily.
[ minor ] inlining a where clause