On Statman's Finite Completeness Theorem

Richard Statman, Gilles Dowek

We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $\lambda$-definability conjecture implies the higher-…