Moved some thms around, proved Raise and fix part of Let