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