Thm* f:(D:Type. D(D List)), A:Type, a,x:A. x list f(a)  x = a

That is, any polymorphic function from D(D List) simply replicates its input value.

Proof:

Suppose f  (D:Type. D(D List)) and a  A.

Then simply specializing the type of f to the singleton {a:A},
we get that f  {a:A}({a:A} List).

Hence every member of f(a)  {a:A} List is simply a  A,

(by a lemma Thm* a:A, w:{a:A} List. z:A. z list w  z = a)

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html