This is true but there is actually an end ;) There are limits on provable equivalence in the first place. things like equality saturation also try and do a be

This is true but there is actually an end ;) There are limits on provable equivalence in the first place. things like equality saturation also try and do a better job of formalizing equivalence based rewrites.