Nuprl - Proof: card curry simple 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card curry simple 1 1

1. A : Type
2. B : Type
3. C : Type

InvFuns(A

C;A

e,x,y. e(<x,y>);

e,z. z/x,y. e(x,y))

By:	Analyze THEN Rename-1: e THEN Reduce Concl

Generated subgoals:

1 4. e : ABC
(z.z/x,y. e(<x,y>)) = e
1 step

2 4. e : ABC
(x,y. e(x,y)) = e
1 step

About:

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

1	4. e : ABC (z.z/x,y. e(<x,y>)) = e	1 step
2	4. e : ABC (x,y. e(x,y)) = e	1 step