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

By:	Def of (x:A. B(x)) ~ (x:A'. B'(x)) | (x:AB(x)) ~ (x:A'B'(x)) THEN ExistHD Hyp:-1

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))   f:((x:AB(x))(x:A'B'(x))), g:((x:A'B'(x))(x:AB(x))).   InvFuns(x:AB(x);x:A'B'(x);f;g)

6 steps

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