Export a helper function in Opentheory

The function tweaks the theorems produced by define_new_type_bijections
to match the (closed) format introduced with article version 6.

Adjust organisation of opentheory files

This is so that files in the build sequence actually get "compiled" in a
context where they might conceivably be loaded. This is a necessary
prerequisite to getting this code compiled under Moscow ML. Sadly,
that's not possible quite yet, but does seem a worthwhile objective
eventually.