Module-ize Iris-Lean #121
Description
Because modules need to be used bottom-up, we should make sure Iris-Lean uses modules so that it's not a problem for any dependencies.
Sebastian gave instructions for how to do this in his Lean Together talk and says it's not much work. We should probably do this when updating to 4.27, where modules are stabilized.
