J. McKinna and R. Pollack, “Some Lambda Calculus and Type Theory Formalized”, BRICS, vol. 4, no. 51, Jun. 1997.