change name append to snoc..
trying on DRF->Well-Synchronized
move on for now, cannot get stuck here all the time
add helper functions
stick to writing flatten as a function; add coherent definition
redefine simulation & drf guarantee theorem