Require

[Rocq] A command in Rocq that loads a compiled module into memory, making its contents available but not directly accessible without qualification.