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

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

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)

f:(X

Z), g:(Z

X). InvFuns(X;Z;f;g)

By:	Analyze9 THEN Analyze5

Generated subgoal:

1 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
f:(XZ), g:(ZX). InvFuns(X;Z;f;g)
3 steps

About:

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