Small cleanups, invariant-theorems are now broken, unfortunately.
Some more documentation.
More documentation.
Leftover theorems.