Requires should always be at the top of a file, Imports can be inside
of submodules.

It is strange that a Require in a submodule is allowed and then triggers
an error when using the whole module. This may be a Coq bug.

They will use Iris is a library, in that paper's repo

...but it does not work. Hu?

The proof is not pretty, though...