first versionof DEF_equal proof (with two admits)
add assertion about separation
resolve two admits
remove old proof attempt
remove final admit in DEF_equal