Admit-free proof of Postponement theorem

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)