IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Thm* 
f:(
D:Type. D
D), A:Type, a:A. f(a) = a
That is, a polymorphic DD must copy its input value.
Proof:
Suppose f 
(D:Type. DD).
f {a:A}{a:A}, by specializing intersection.
But a is the only member of {a:A}, so
f(a) = a A
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
