Improve expression equality performance

[ctrekker]

Now that a list of parents is preserved, mutations made at the roots of an expression tree can propagate upwards, meaning that there is no longer a need to descend all the way down an expression tree each time :(==) is called. About half of all proof algorithm time is spent comparing expressions right now!!