Explore use of `#[local]`/`Local` definitions
I recently learned that in Coq, we can mark a definition as not being imported with Import/Export. I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, consider these.
Local Definition is supported in Coq 8.9 (and maybe older) so we can start using it any time.