(11steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr fams trans 1
1. A : Type
2. A' : Type
3. A'' : Type
4. B : AType
5. B' : A'Type
6. B'' : A''Type
7. (x:A. B(x)) ~ (x':A'. B'(x'))
8. (x':A'. B'(x')) ~ (x'':A''. B''(x''))
  (x:A. B(x)) ~ (x'':A''. B''(x''))
By: (7) Def THEN ExistHD Hyp:7 THEN (-1) Def THEN ExistHD Hyp:-1

Generated subgoal:

1 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''))
9 steps

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

(11steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc