EGG, from "Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation"

Equality saturation is pretty cool as a technique for exploring a large space efficiently by exploiting its peculiar structure!