A,A':Type, B:(AType), B':(A'Type).
  (x:A. B(x)) ~ (x:A'. B'(x))  ((x:AB(x)) ~ (x:A'B'(x)))

1

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))   (x:AB(x)) ~ (x:A'B'(x))

8 steps

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