simplify squash_to_set

and learn some useful lemmas about null homotopies by splitting them
off from the proof, which is now much smaller