Disable the use of ExistCircuit

Not working correctly, at least for the SMTSerial backend
Do another round of subterm criterion every time

It’s cheap
- I should find the time to trim the proof trees to remove intermediate
steps with no changes
- Instead of another round, should do it in a fixpoint