Remove dependency between `BUILTIN` and postulates

[fredrik-bakke]

This PR is preparation for #1379.

The BUILTIN pragma cannot be invoked inside of a parametrized module, which in practice means that we cannot have a dependency on an axiom in a module where a BUILTIN is invoked. This PR resolves that by moving dependencies around and splitting a couple of files into smaller parts.

[fredrik-bakke]

After some preliminary experimentation, there are some technical issues to point out:

• Named modules with parameters are incompatible with BUILTIN pragmas, so I've refactored all modules that have such a pragma to depend only on files that are not (transitively) dependent on any module that uses funext anywhere.
• There's an issue with public imports when using named imports. See the current typechecking error. Essentially, such definitions are duplicated in the scope, leading to "ambiguous names"

[fredrik-bakke]

The python scripts will be removed later.

EDIT: Removed

[fredrik-bakke]

I've refactored all modules that have such a pragma to depend only on files that are not (transitively) dependent on any module that uses funext anywhere.

*If we get to that stage, I can pull these changes to a different branch for a separate review later.