Nuprl - Proof: one one corr is equiv rel 3

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

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

f1:(X

Y), g1:(Y

X). InvFuns(X;Y;f1;g1)
4. Z : Type
5.

f2:(Y

Z), g2:(Z

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

f:(X

Z), g:(Z

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

By:	ExistHD Hyp:5 THEN ExistHD Hyp:3

Generated subgoal:

1 3. f1 : XY
4. g1 : YX
5. InvFuns(X;Y;f1;g1)
6. Z : Type
7. f2 : YZ
8. g2 : ZY
9. InvFuns(Y;Z;f2;g2)
f:(XZ), g:(ZX). InvFuns(X;Z;f;g)
4 steps

About:

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