Materialize Equality

[marcusrossel]

We currently only reflect, but do not materialize equality. The latter can be necessary though, e.g. if we have a rewrite like $\forall P, \neg (P = \bot) \to P = \top$. If this is applied to a term where $P = eq t_1 t_2$, then we end up merging $eq t_1 t_2$ into $\top$, without $t_1 = t_2$ being materialized in the e-graph.
As an approach to materialization which is more efficient than $\forall x y, ((x = y) = \top) \to x = y$, we could add a hook into our rewrites which checks if the final union_instantiations involves an eq, and if so adds the materialization.