The last theorem above states that VoidA has only the one member (x.x). This is a degenerate function in that it cannot be applied to anything in Void. Indeed, the body of the function expression is irrelevant since it will never be evaluated as part of application to any argument of type Void.

So, although VoidA has only one member, every (closed) lambda expression denotes that member. See Functions.

Similarly, the intersection over the empty domain is a trivial one-element type whose single member is denoted by every expression that can denote at all: