  We advocate the use of de Bruijn's universal abstraction $\lambda^\infty$ for
the quantification of schematic variables in the predicative setting and we
present a typed $\lambda$-calculus featuring the quantifier $\lambda^\infty$
accompanied by other practically useful constructions like explicit
substitutions and expected type annotations. The calculus stands just on two
notions, i.e., bound rt-reduction and parametric validity, and has the
expressive power of $\lambda\rightarrow$. Thus, while not aiming at being a
logical framework by itself, it does enjoy many desired invariants of logical
frameworks including confluence of reduction, strong normalization,
preservation of type by reduction, decidability, correctness of types and
uniqueness of types up to conversion. This calculus belongs to the
$\lambda\delta$ family of formal systems, which borrow some features from the
pure type systems and some from the languages of the Automath tradition, but
stand outside both families. In particular, the calculus includes and evolves
two earlier systems of this family. Moreover, a machine-checked specification
of its theory is available.
