Nuprl - Proof: delete fenum value is fenum 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value is fenum 1 1

1. m :

2. k :

3. f :

(m+1)

(k+1)
4. Inj(

(m+1);

(k+1); f)
5. Surj(

(m+1);

(k+1); f)

Inj(

k; Replace value k by f(m) in f)

By:	BackThru: Thm* Inj((m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f)

Generated subgoals:

None

About:

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