1. A : Type
2. B : Type
3. (fg.fg/f,g. <f,g,(x.*),(y.*)>)  (AB)(A ~ B)
4. (fga.fga/f,#. #/g,a. <f,g>)  (A ~ B)AB
5. f : AB
6. g : BA
7. a1 : x:A. g(f(x)) = x
8. a2 : y:B. f(g(y)) = y
  <x.*,y.*> = <a1,a2>  ((x:A. g(f(x)) = x) & (y:B. f(g(y)) = y))

1	(x.*) = a1	3 steps
2	(y.*) = a2	4 steps

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