Make [ELCtx_Alive] a coercion

I made ELCtx_Alive a coercion.

This has several consequences:

• lft has to be a definition instead of a notation. In order to make sure that it will not be unfolded, I made it part of the signature of the lifetime logic
• The parameters of the fn type have to be uncurried, so that the type inference of Coq determines the value of A befor type-checking the external lifetime environment.

What do you think? Is it worth merging as-is or should we use a notation after all?