Relaxing the sort elimination check to allow for let-bindings in arities.

I restored this in the kernel, and added it to the checker. There is one last
source of non-uniformity, which is the Sort case in the checker (was not
present in the kernel). I don't know what this case covers, so it should be
reviewed.