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

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

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

By:	False Asserted THEN Rewrite'7 by Thm: delete fenum value comp1 Using:[i:= a1] THEN Rewrite'7 by Thm: delete fenum value comp2

Generated subgoal:

1 7. f(m) = f(a2) k
8. f(a1) = k
9. f(a2) = k
False
1 step

About:

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