On Statman's Finite Completeness Theorem
Richard Statman, Gilles Dowek · arXiv (Cornell University) · 2023
We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $λ$-definability conjecture implies the higher-order matching conjecture.