Nuprl - Proof: nsub bij ooc invpair 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij ooc invpair 1 1 1

1. a :

2. f :

a bij

<f,

y.least x:

. f(x)=

By:	Guarding (least [var]:. <bool>) Analyze THEN Reduce Concl

Generated subgoals:

1 <f,y.least x:. f(x)=y> (aa)(aa)
3 steps

2 InvFuns(a;a;f;y.least x:. f(x)=y)
1 step

About:

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

1	<f,y.least x:. f(x)=y> (aa)(aa)	3 steps
2	InvFuns(a;a;f;y.least x:. f(x)=y)	1 step