Nuprl - Proof: card product swap 1

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

1. A : Type
2. B : Type

f:(A

A), g:(B

B). InvFuns(A

B;B

A;f;g)

By:	(yx.yx/y,x. <x,y>)((xy.xy/x,y. <y,x>)(<x,y>)) * <x,y>

Generated subgoals:

None

About:

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