Make [ELCtx_Alive] a coercion
ELCtx_Alive a coercion.
This has several consequences:
lfthas 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
fntype have to be uncurried, so that the type inference of Coq determines the value of
Abefor type-checking the external lifetime environment.
What do you think? Is it worth merging as-is or should we use a notation after all?