Nuprl - Proof: increasing inj 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: increasing inj 1 1 1

1. k :

2. m :

3. f :

m
4. increasing(f;k)
5. a1 :

k
6. a2 :

k
7. f(a1) = f(a2)
8.

x,y:

k. x<y

f(x)<f(y)
9. a1<a2

a1 = a2

By:	FwdThru -2 [-1]

Generated subgoals:

None

About:

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