The equality operator terminates as early as it can. Any speed up you got was most likely because you checked the term in an order that happened to be more efficient (equality check uses DFS IIRC).
The equality operator terminates as early as it can. Any speed up you got was most likely because you checked the term in an order that happened to be more efficient (equality check uses DFS IIRC).