McKinna, J. and Pollack, R. (1997) “Some Lambda Calculus and Type Theory Formalized”, BRICS Report Series, 4(51). doi: 10.7146/brics.v4i51.19272.