(9steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card sigma 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))
  InvFuns(x:AB(x);x:A'B'(x)
  InvFuns;e.e/x,y. <f(x),F(x,y)>;e.e/x,y. <g(x),G(g(x),y)>)
By: Analyze THEN Rename-1: e THEN New:[x | y] Analyze-1 THEN Reduce Concl

Generated subgoals:

1 11. x : A
12. y : B(x)
  <g(f(x)),G(g(f(x)),F(x,y))> = <x,y>  x:AB(x)
3 steps
2 11. x : A'
12. y : B'(x)
  <f(g(x)),F(g(x),G(g(x),y))> = <x,y>  x:A'B'(x)
3 steps

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

(9steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc