Polish pred_setTheory with new rewrites for CARD applied to DIFF and UNION.

Preserve old theorems for the sake of backwards compatibility, so give
new theorems names with _EQN as suffix.