Guidi, F. Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. JFR 2012, 5, 1-25.