Abstracting the handling of fresh variables

  In order for fresh variable generation to be more reliable, we
  moved to a more abstract setting. Functions where name generation
  is needed now mention it in their type. Hightlight of the changes:

  `Fresh m a = State a (m a)` relies on the State monad to propagate
  the current next name. ̀fresh` is defined once and for all and makes
  sure that the state is updated.

  The closures built in the model now explicitly say that some of their
  subterms may have been generated using (un)quote as witnessed by their
  codomains.

  The more polymorphic types given to evaluation and (un)quote allowed
  for a really nice typechecker-driven refactoring phase. As soon as
  the typechecking errors were fixed, `Test`s were running perfectly fine.
  Just as before these important modifications.