finish most of the proof of DRF->Well-Synchronized
add some thoughts to the rest of DRF->Well-Synchronized proof