Some small performance improvements

[ryandancy]

• Simplifier wouldn't recurse through eq/app/closure because they should be atomic; however, if one side of an equality (for example) is an ITE, there could be major simplifications. So recurse through there.
• Fix a condition in OPFI where encountering ITEs would cause the term size to blow up with lots of unnecessary guards, which occurred when dealing with the ordering module. Now a guard is not generated if there are no integers involved.

[otzzila]

The opfi optimization looks good to me.