add theorem about dfunion on FEMPTY
add some more automatic rewrites