1. A : Type
2. A' : Type
3. B : AType
4. B' : A'Type
5. f : AA'
6. g : A'A
7. F : x:AB(x)B'(f(x))
8. G : x:AB'(f(x))B(x)
9. InvFuns(A;A';f;g)
10. u:A. InvFuns(B(u);B'(f(u));F(u);G(u))
  F:(x':A'B'(x')B(g(x'))), G:(x':A'B(g(x'))B'(x')).
  InvFuns(A';A;g;f) & (u:A'. InvFuns(B'(u);B(g(u));F(u);G(u)))

By:	G o g  x':A'B'(x')B(g(x')) | F o g  x':A'B(g(x'))B'(x')  Asserted

1	G o g  x':A'B'(x')B(g(x'))	2 steps
2	11. G o g  x':A'B'(x')B(g(x'))   F o g  x':A'B(g(x'))B'(x')	2 steps
3	11. G o g  x':A'B'(x')B(g(x')) 12. F o g  x':A'B(g(x'))B'(x')   F:(x':A'B'(x')B(g(x'))), G:(x':A'B(g(x'))B'(x')).   InvFuns(A';A;g;f) & (u:A'. InvFuns(B'(u);B(g(u));F(u);G(u)))	7 steps

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