[ refactoring ] isolating mu bound & lam/pi bound

* I have decided to isolate mu bound variables (used in descriptions)
  from lam / pi bound ones (used in types / terms) in order to have
  a proper variable mechanism for descriptions (thus allowing for
  nested mus).

* I have tried to explore the idea that pi and sigma abstraction
  should quantify over mu-closed types but could not come up with a
  working system.

* There are still quite a lot of "undefined" lurking around but this
  is the first instance that makes it possible to typecheck simple
  expressions:

    `checkNf empty nat zro`
    `checkNf empty nat $ suc zro`

  are both fully working.