tuned proofs: avoid implicit prems;
major cleanup of proofs/document;
By chapter:chapters 1 and 2, maybe 3: Peter Whitechapters 6, 7 and 8: David von Oheimchapter 6, maybe 8: Gerwin Kleinchapters 3, maybe 4: Tanja Voschapters 1-3 at least: Stefano Bistarelli