Clarify rules restricted when generated from CVC4

Haniel indicated that some rules are generated in a stricter variant by CVC4. It is unclear how we will enable reconstructions to benefit from this without writing solver specific routines.

The two big options are: a) have a dedicated rule for the more specialized version b) have optional arguments.

It is probably best to first collect those cases.