Move stages of garbage collection to proof framework, and add obligations subsection
Definition of general correctness: it's almost identical to what we had before (and probably could have been totally identical)