Support type aliases

[janmasrovira]

Fixes #1349 and #1342 and #1333.

this PR adds the ability to define type aliases. More generally, it adds limited normalization to the language.
The set of function definitions that support normalization are of the following form:

f : .. -> Type;
f x y z := ...;

More precisely, a function f supports normalization iff:

1. It has a single clause.
2. The return type is Type.
3. It has no patterns matching implicit arguments (probably trivial to remove this restriction).
4. All patterns are variables (allowing wildcards should be easy to add).

[janmasrovira]

We need to fix positivity checking when the constructor types use type functions. Should we do it in this PR or in another one?