Nuprl - Proof: nsub bij ooc invpair 1 2

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

1. a :

2. (

f.<f,

y.least x:

. f(x)=

y>)

(

a bij

(

fg.fg/f,g. f)

(

a bij

By:	Analyze THEN Analyze-1 THEN New:[f \| g] Analyze-2 THEN OnAllClauses Reduce THEN Analyze

Generated subgoal:

1 3. f : aa
4. g : aa
5. InvFuns(a;a;f;g)
Bij(a; a; f)
1 step

About:

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