Use purification for set comprehension reduction (#8711)

Use purification for set comprehension reduction (#8711)

Currently, the reduction lemma does not purify set comprehension from its reduction predicate. This means that our rewriter (if it were smart enough) should rewrite the reduction predicate to true.

Moreover, a new forthcoming model-based instantiation technique was giving wrong answers when set comprehensions were present since it could prove the reductions were tautological.