New notation : typed_val.

This simplifies the statements of all the toplevel typing theorem, and make them generic on the lifetime contexts, so that they can actually be used.