Depostulate function extensionality

[fredrik-bakke]

No description provided.

[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.

[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.