Nuprl - Proof: not nat occ natfuns 1 1 1 1 1

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

1. (

) ~

2. f :

3. Inj(

;

; f)
4. Surj(

;

; f)
5. a :

6. f(a) = (

i.f(i,i)+1)

False

By:	ApFun: Hyp:-1 to: a

Generated subgoal:

1 7. f(a,a) = f(a,a)+1
False
Auto

About:

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