Master into Types

Types should be integrated into the theorem system. This will be done in the types topic branch, then brought back into master once the integration is complete.