Very serious bug fixed in unification, but the fix is very ugly.

Very serious bug fixed in unification, but the fix is very ugly.

Explanation: we have reduced the case ? x1 .. xn to the case
?[x1,...,xn] by mean of lambda-abstractions. However, these need to be
typed. The way we used to type them was with non-dependent types. Thus they
failed in almost all dependent cases (like rewrite).

This fix seems to work and uses a few lines of code, but it requires a call
to the unifier which is VEEERY bad.

Debugging prints still to be removed.