PfPrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Thm* f:(D:Type. DT), A:Type, a:AB:Type, b:Bf(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:
isectfunctionuniverseequalmembertopall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PfPrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc