Nuprl - Proof: disjoint increasing onto 1 1 1 1 2 1 1 1

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

1. m :

2. n :

3. k :

4. f :

m
5. g :

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

(j:

i = f(j))+(j:

i = g(j))
9.

j1:

n, j2:

f(j1) = g(j2)
10. a1 :

m
11. a2 :

m
12. j :

n
13. x1 : a1 = f(j)
14. h(a1) = inl(<j,x1>)
15. j1 :

n
16. x2 : a2 = f(j1)
17. h(a2) = inl(<j1,x2>)
18. j = j1

a1 = a2

By:	HypSubstSq -3 0 THEN HypSubstSq -6 0 THEN Analyze

Generated subgoals:

None

About:

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