Added more to the argument of correctness for delimited control, plus a discussion of similarity with CFA2's approach for call/cc.
Proof for PDCFA finished?