Galdino, A. L.; Ayala-Rincón, M. A Formalization of Newman’s and Yokouchi’s Lemmas in a Higher-Order Language. JFR 2008, 1, 39-50.