Fixing two serious loop bugs in relevance typing

The first bug was caused by some serius misunderstanding of how lamdbas are
generated. Now we pop and push environments properly. Should be fine.
The second bug was the lack of "proper" handling of recursive lets.
Proper typing in recursion might not be possible, but we at least do not
crash/halt/dance forever when we meet them.
Improving substitution in relevance typing.

Most of the required (including the final) substitutions were not being properly
performed. This should fix it.