Cleaned up the reference-compare proof
Added theorem for colletive exhaustion property. Sketched in more details for the summary initialization lemma.