1. A : Type
2. A' : Type
3. A'' : Type
4. B : AType
5. B' : A'Type
6. B'' : A''Type
7. f : AA'
8. g : A'A
9. F : x:AB(x)B'(f(x))
10. G : x:AB'(f(x))B(x)
11. InvFuns(A;A';f;g)
12. u:A. InvFuns(B(u);B'(f(u));F(u);G(u))
13. f1 : A'A''
14. g1 : A''A'
15. F1 : x':A'B'(x')B''(f1(x'))
16. G1 : x':A'B''(f1(x'))B'(x')
17. InvFuns(A';A'';f1;g1)
18. u:A'. InvFuns(B'(u);B''(f1(u));F1(u);G1(u))
  (x:A. B(x)) ~ (x'':A''. B''(x''))

By:	Witness: f1 o f | g o g1 | x.F1(f(x)) o F(x) | x.G(x) o G1(f(x)) THEN Reduce Concl

1	InvFuns(A;A'';f1 o f;g o g1)	4 steps
2	19. u : A   InvFuns(B(u);B''(f1(f(u)));F1(f(u)) o F(u);G(u) o G1(f(u)))	4 steps

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