Add support for inferred binders in terms

We should be able to compile the following program:

id' :: forall {a}. a -> a
id' x = x

And get the kindchecked and translated type: id : \forall {a : Type}. a -> a