(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: injection type functionality wrt ooc 1 1 3

1. A : Type
2. A' : Type
3. B : Type
4. B' : Type
5. f1 : AA'
6. g1 : A'A
7. InvFuns(A;A';f1;g1)
8. f : BB'
9. g : B'B
10. InvFuns(B;B';f;g)
11. x:Bg(f(x)) = x
12. y:B'f(g(y)) = y
13. x:Ag1(f1(x)) = x
14. y:A'f1(g1(y)) = y
15. Inj(AA'f1)
16. Inj(A'Ag1)
17. Inj(BB'f)
18. Inj(B'Bg)
19. (h.f o h o g1 (A inj B)A' inj B'
20. (h.g o h o f1 (A' inj B')A inj B
  InvFuns(A inj B;A' inj B';h.f o h o g1;h.g o h o f1)


By: Analyze THEN Reduce Concl


Generated subgoals:

1 21. x : A inj B
  g o f o x o g1 o f1 = x  A inj B

5 steps
2 21. y : A' inj B'
  f o g o y o f1 o g1 = y  A' inj B'

1 step

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

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc