Guidi, Ferruccio. 2012. “Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover”. Journal of Formalized Reasoning 5 (1):1-25. https://doi.org/10.6092/issn.1972-5787/3392.