A. Rauber Du Bois, R. Ribeiro, and M. Amaro, “A Mechanized Proof of a Textbook Type Unification Algorithm”, RITA, vol. 27, no. 3, pp. 13–24, Jun. 2020.