Rauber Du Bois, André, et al. “A Mechanized Proof of a Textbook Type Unification Algorithm”. Revista De Informática Teórica E Aplicada, vol. 27, no. 3, June 2020, pp. 13-24, doi:10.22456/2175-2745.100968.