Always purify universe from set minus (#8201)

Always purify universe from set minus (#8201)

This fixes a bug in our handling of set cardinality + set universe (also used for set complement).

The bug was caused by using the rewritten form of terms to compute siblings in the cardinality graph. This is problematic for
(set.minus set.universe t) whose sibling was computed to be rewrite( (set.inter set.universe t) ) = t.

To avoid the issue, we now purify the argument of set.minus to avoid this behavior.

Fixes #5400.
Fixes the first benchmark on #5402.

This also eliminates a spurious lemma schema for set universe that was leftover from handling set subtyping.