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))
11. x : A
12. y : B(x)
  <g(f(x)),G(g(f(x)),F(x,y))> = <x,y>  x:AB(x)

By:	g(f(x)) = x  A  By BackThru: Hyp:9 THEN ApFun: x.B'(f(x)) to: g(f(x)) = x  A THEN Rewrite by g(f(x)) = x  A

1

13. g(f(x)) = x 14. B'(f(g(f(x)))) = B'(f(x))   <x,G(x,F(x,y))> = <x,y>  x:AB(x)

2 steps

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