Thm*  a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))

This priniciple very nearly tells us that if we assign to each MEMBER of a finite class, another finite class, then we can count the pairs of the dependent-pair-type by simply adding up the sizes of all the classes in the family of classes.

(to be continued later - sfa)

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html