  We give an arithmetical proof of the strong normalization of the
$\lambda$-calculus (and also of the $\lambda\mu$-calculus) where the type
system is the one of simple types with recursive equations on types. The proof
using candidates of reducibility is an easy extension of the one without
equations but this proof cannot be formalized in Peano arithmetic. The strength
of the system needed for such a proof was not known. Our proof shows that it is
not more than Peano arithmetic.
