add proof that normal forms can be typed by intersection types

Also remove the scratch.tex file as it is now redundant.
reorder sections

This way the paper can be read sequentially, and all the results that can be presented without introducing a typing system
are done first, to make the distinction clear.
delete some left-over derivations

These were never meant to be added.