Nuprl - Proof: one one corr is equiv rel 3 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr is equiv rel 3 1 1 2

1. X : Type
2. Y : Type
3. f1 : X

Y
4. g1 : Y

X
5. InvFuns(X;Y;f1;g1)
6. Z : Type
7. f2 : Y

Z
8. g2 : Z

Y
9. InvFuns(Y;Z;f2;g2)
10.

x:Y. g2(f2(x)) = x
11.

y:Z. f2(g2(y)) = y
12.

x:X. g1(f1(x)) = x
13.

y:Y. f1(g1(y)) = y
14. y : Z

f2(f1(g1(g2(y)))) = y

By:	Rewrite by Hyp:13 THEN Rewrite by Hyp:11

Generated subgoals:

None

About:

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