Thm* T:Type, f:(D:Type. DT). f(f)  T

An expression of polymorphic function type "D:Type. DT" denotes both a function and a value of its domain.

By specializing f  (D:Type. DT)

in two ways we may infer both

f  TT and f  (TT)T, hence f(f)  T.

It would be misleading to say that a function can be applied to itself, however. Although the same expression may appear as both function and argument in f(f), the two occurrences denote values of different types. The apparent "self-application" is merely syntactic.

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