Nuprl - Proof: delete fenum value wf 1 1 1 1

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

1. m :

2. k :

3. f :

(m+1)

(k+1)
4. Inj(

(m+1);

(k+1); f)
5. i :

m
6. f(i) = k

f(m) = k

By:	m = i Asserted

Generated subgoal:

1 7. m = i
f(m) = k
2 steps

About:

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