Nuprl - Proof: disjoint increasing onto 1 2

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

1. m :

2. n :

3. k :

4. f :

m
5. g :

m
6. increasing(f;n)
7. increasing(g;k)
8.

m. (

n. i = f(j))

(

k. i = g(j))
9.

j1:

n, j2:

f(j1) = g(j2)
10. m

n+k

m = n+k

By:	Assert (n+km)

Generated subgoals:

1 n+km
7 steps

2 11. n+km
m = n+k
Auto

About:

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