Fixed the wrap case in the type checker

[effectfully]

This fixes another bunch of bugs in the type checker which finally allows us to type check the standard library.

It also showcases how we should comment each of the cases:

    -- G |- term : nTermTy, ty ~>* nTy, [fix n nTy / n] nTy ~>* nTermTy', nTermTy ~ nTermTy'
    -- -------------------------------------------------------------------------------------
    -- G |- wrap n ty term : fix n nTy

I'll write more on that on the mailing list, but hey, we can type check the standard library.

[vmchale]

This will be superseded by the new elimination contexts, yes?

[effectfully]

Elimination contexts shouldn't throw this away and should instead adapt the rule and the implementation.

[vmchale]

In that case, we should update the spec as well, yes?

[effectfully]

The spec is not of algorithmic nature while the code obviously is. I don't know whether the spec should be updated or not.

[vmchale]

This changes the places we do reductions, yes? That is different from the old spec.

[mchakravarty]

The spec really needs two versions of the type synthesis: (1) a declarative one that may not be explicit about where reductions happen and (2) an algorithmic one that is explicit about it. This is what we did agree on during the meeting. I hope @psygnisfive will have a chance to add this to the spec soon.