also strengthen local lifetime context to not add laters in front of the inherited ownership

change cont_postcondition to True... because we can, and because that would allow us to show adequacy with a terminating continuation

This (finally) requries us to add thread-local tokens to various judgments