Cancellable elements.

I propose to create a typeclass for a notion of cancellable elements.

They are a generalization of exclusive elements (i.e., any exclusive is cancellable), that allows new ways of proving local updates. In principle, we could use this new reasoning principle instead of the one based on Exclusive for deallocating elements from a map.

Even though I haven't tested that everything works well until the end, it seems that this is needed for proving soundness of drop for a Ref in Lambdarust.

Things gets a little bit subtle in the actual implementation, because there are actually two notions of cancellability, depending on whether we want to forbid x = x . y or not for x cancellable. Fortunately, it appears that the strong variant of cancellability of coincide with the cancellability of (Some x), so that we can use the same definition.