Thm* f:(C,D:Type. CDDC), A,B:Type, a:A, b:B. f(<a,b>) = <b,a>  BA

That is, a polymorphic CDDC must swap its pair of input values.

Proof:

Suppose f  (C,D:Type. CDDC).

f  {a:A}{b:B}{b:B}{a:A}, by specializing intersection.

But <b,a> is the only member of {b:B}{a:A}, so

f(<a,b>) = <b,a>  BA

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