Thm* f:(D:Type. D(D List)), A:Type, a:A, B:Type, b:B.
Thm* ||f(a)|| = ||f(b)||  

That is, the length of a list produced by a polymorphic D(D List) function is independent of the input value.

Proof:

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

Then the composition of f with list length, i.e. (x.||f(x)||), is of type (D:Type. D),

and so our goal follows from the lemma

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

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