Shorten rexcom

[wlammen]

1. shorten rexcom
2. shorten rexim. The current proof uses the ¬ symbol 12 times, two times more than necessary. Reducing the symbol count in the proof display is a valid shortening. I did not create a tag or an OLD version for this minor change.
3. reuanid seems to me misplaced amidst ral* and rex* theorems. Move it to the area dedicated to rmo*/reu* theorems
4. The section developing theorems around df-ral and df-rex does not look very tidy to me. It mixes theorems covering different aspects in the same places. The way I search the database systematically suggests, theorems based on df-ral only, respective df-rex only, should have their own area, followed by theorems mixing both ideas. In this sense I separated ralcom* and rexcom*, hopefully finding a more intuitive location for both.
5. Delete outdated OLD theorems.