Author: Tobias Nipkow Copyright 1992 University of Cambridge Barendregt's Lambda-Cube. NB: the formalization is not completely sound! It does not enforce distinctness of variable names in contexts! For more information about the Lambda-Cube, see H. Barendregt, Introduction to Generalised Type Systems, J. Functional Programming.