  The formal system $\lambda\delta$ is a typed lambda calculus derived from
$\Lambda_\infty$, aiming to support the foundations of Mathematics that require
an underlying theory of expressions (for example the Minimal Type Theory). The
system is developed in the context of the Hypertextual Electronic Library of
Mathematics as a machine-checked digital specification, that is not the formal
counterpart of previous informal material. The first version of the calculus
appeared in 2006 and proved unsatisfactory for some reasons. In this article we
present a revised version of the system and we prove three relevant desired
properties: the confluence of reduction, the strong normalization of an
extended form of reduction, known as the "big tree" theorem, and the
preservation of validity by reduction. To our knowledge, we are presenting here
the first fully machine-checked proof of the "big tree" theorem for a calculus
that includes $\Lambda_\infty$.
