shorten proofs

[wlammen]

1. shorten cbvralsvw, cbvrexsvw
2. revise rexeq, so that it is directly proven from dfcleq. It is now placed in front of all theorems handling the replacement of the restricting set by an equal one. raleq is proven next. The reason for this order is that there is no correspondence for alexbii for the all quantification, making the proof for rexeq shorter.
3. The former starting points raleqbidvv and rexeqbidvv now have a very short proof. The savings in this rearrangement of theorems sum up to 61 proof bytes in total. On top, having a simple theorem heading a section looks nicer and gives a better feeling for where everything is rooted in.

[icecream17]

edit: wrong, see next comment

cbvralsvw/cbvrexsvw now have a DV on x,y

could the OLD versions be kept as ALT? Since it is not currently useful in main set.mm, perhaps they could be moved to my mathbox (section "Exemplar theorems")

Or I'll do it in my next pr

[wlammen]

The old proof has a DV on x, y, too, so this is no regression. It needs it in line 5 of the old proof cbvralsvw