fixing the universe problems (fingers crossed)

- there is no denotation function denoting expressions
  into typ0 because it seems to require unlifting which
  Coq does not permit.