Added unfold type rule in a comment.
Allow meta variables in type expressions.
More on the implementation of type rules.
Minor stuff.