Thm* f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b)  T

That is, a purely polymorphic DT function is a constant function, and is independent of the input type.

Proof:

Suppose f  (D:Type. DT), a  A, and b  B.

f  TopT, by specializing intersection;

and a = b  Top,

hence f(a) = f(b)  T.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html