updated the Delay stuff with Tarmo's suggestions, only proved it's a monad using termination sensitive weak bisimularity, nothing else.
modified:   PartialDelay.agda