A. L. Galdino and M. Ayala-Rincón, “A Formalization of Newman’s and Yokouchi’s Lemmas in a Higher-Order Language”, JFR, vol. 1, no. 1, pp. 39–50, Jan. 2008.