(9steps total) Gloss PrintForm NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc type poly swap
  f:(C,D:Type. CDDC), A,B:Type, a:A, b:B. f(<a,b>) = <b,a>
By: Auto

Generated subgoal:

1 1. f : C,D:Type. CDDC
2. A : Type
3. B : Type
4. a : A
5. b : B
  f(<a,b>) = <b,a>
8 steps

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

(9steps total) Gloss PrintForm NuprlPrimitives Sections NuprlLIB Doc