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