Nuprl - Proof: delete fenum value is fenum 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: delete fenum value is fenum 1 2 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)
6. b :

k
7. a :

(m+1)
8. f(a) = b
9. c :

(m+1)
10. f(c) = k

m. (Replace value k by f(m) in f)(a) = b

By:	Decide: a = m (m+1)

Generated subgoals:

1 11. a = m  (m+1)
  a:m. (Replace value k by f(m) in f)(a) = b
2 steps

2 11. a = m  (m+1)
  a:m. (Replace value k by f(m) in f)(a) = b
1 step

About:

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

1	11. a = m (m+1) a:m. (Replace value k by f(m) in f)(a) = b	2 steps
2	11. a = m (m+1) a:m. (Replace value k by f(m) in f)(a) = b	1 step