It is not a library; it does not contain code, but instead is a core
part of heap_lang.

Thanks to Amin Timany for the suggestion.

Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction

This allows us to move the \later in the user-defined functor to any place we want.
In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.

Tactics like wp_proj should always solve all to_val side-conditions. The
tactic wp_done is used to handle these in a uniform way.