Differentiation and equality checking through e-graphs/simplification is already supported. But it's not done automatically with the symbolic-numeric integratio

Differentiation and equality checking through e-graphs/simplification is already supported. But it's not done automatically with the symbolic-numeric integration: you'd have to call it after the integration to check which terms are necessary. We could probably improve the algorithm by doing this automatically and then doing more trimming of some sort.