  We consider the following decision problem: given two simply typed
$\lambda$-terms, are they $\beta$-convertible? Equivalently, do they have the
same normal form? It is famously non-elementary, but the precise complexity -
namely TOWER-complete - is lesser known. One goal of this short paper is to
popularize this fact.
  Our original contribution is to show that the problem stays TOWER-complete
when the two input terms belong to Blum and Ong's safe $\lambda$-calculus, a
fragment of the simply typed $\lambda$-calculus arising from the study of
higher-order recursion schemes. Previously, the best known lower bound for this
safe $\beta$-convertibility problem was PSPACE-hardness. Our proof proceeds by
reduction from the star-free expression equivalence problem, taking inspiration
from the author's work with Pradic on "implicit automata in typed
$\lambda$-calculi".
  These results also hold for $\beta\eta$-convertibility.
