Refactoring of initial lemmas in datatypes (#8666)

Refactoring of initial lemmas in datatypes (#8666)

This is work towards revising how/when the datatypes instantiate rule is applied.

This simplifies the management of when new terms are registered in the theory of datatypes.

We now use the equality engine's eqNotifyNewClass callback to know when a term should be considered. Previously, this was split over two methods (additionally, collectTerms).

Most importantly, this eliminates the need for a manual addition of the "instantiated constructor term" in getInstantiateCons, which complicates the logic for the impact of applying the datatypes instantiate rule.