separate transformations for intros, dequant, and remove_unused
This MR should resolve the problem of unused symbols seen in the IDE, and also the regressions on proofs due to too many extra symbols.
This MR should resolve the problem of unused symbols seen in the IDE, and also the regressions on proofs due to too many extra symbols.