Proof of Postponement theorem and remove all admits

Guess what, I managed to push it all the way. I think I have ridiculous amounts of code duplication, but what the hell.

(Subsumes #19)