As far as I know, two lambda terms are equal if and only if their normal forms can be $\alpha$ converted to each other.
However, for expressions that do not have a normal form (such as expressions involving a Y combinator), are there any rules to let us state two expressions are equal?
I originally thought of this problem when I tried to figure out whether $(Y\ f)$ equals $(Y\ (f\circ f))$ (where $f\circ f=\lambda x.\ f\ (f\ x)$), but I can neither prove it nor find an exception to the formula.