Nuprl - Proof: nat not finite 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat not finite 1 1 1

1. n :

2. f :

n
3. g :

4. InvFuns(

;

n;f;g)

(n+1)

By:

Analyze-1

Generated subgoal:

1 4. x:. g(f(x)) = x
5. y:n. f(g(y)) = y
~ (n+1)
4 steps

About:

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