Use constants to reduce the size of translated terms

[sacerdot]

Alfiarao has implemented setSigma in his own clone. However, it is clear that the size of the translated term grows way to much. An approach to the problem is to implement definition schemas (i.e. a real library) and use it to reduce the size of the translation. Alfiarao is trying to do that. It's not easy because the type theory need schemas (it has no quantification over types) over types bus also over dependent types.