Guidi, Ferruccio. “Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover”. Journal of Formalized Reasoning 5, no. 1 (January 1, 2012): 1–25. Accessed September 29, 2022. https://jfr.unibo.it/article/view/3392.