Add both non-expansive and contractive functors, and bundle them for the...

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.
1 job for master
Status Job ID Name Coverage
  Test
passed #195
coq
buildjob

00:03:19