IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
delete fenum value is inj114 1. m :
2. k :
3. f : (m+1)(k+1)
4. Inj((m+1); (k+1); f)
5. a1 : m 6. a2 : m 7. (Replace value k by f(m) in f)(a1) = (Replace value k by f(m) in f)(a2)
8. f(a1) = k 9. f(a2) = k a1 = a2