remove some dead code, beautify other code, comment out some unusued code, and fix a bug in swapDownFrom
simplify some proofs
merge and simplify