Nuprl - Proof: one one corr is equiv rel 3 1 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

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

f:(X

Z), g:(Z

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

By:	Witness: f2 o f1 \| g1 o g2 THEN Analyze THEN Reduce 0

Generated subgoals:

1 14. x : X
g1(g2(f2(f1(x)))) = x
1 step

2 14. y : Z
f2(f1(g1(g2(y)))) = y
1 step

About:

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

1	14. x : X g1(g2(f2(f1(x)))) = x	1 step
2	14. y : Z f2(f1(g1(g2(y)))) = y	1 step