1. m : 
2. n : 
3. k : 
4. f : nm
5. g : km
6. increasing(f;n)
7. increasing(g;k)
8. h : i:m(j:ni = f(j))+(j:ki = g(j))
9. j1:n, j2:k. f(j1) = g(j2)
10. a1 : m
11. a2 : m
  InjCase(h(a1); p. 1of(p), n+1of(p))
  =
  InjCase(h(a2); p. 1of(p), n+1of(p))
   (n+k)
  
  a1 = a2

1

12. q1 : (j:na1 = f(j))+(j:ka1 = g(j)) 13. h(a1) = q1 14. q2 : (j:na2 = f(j))+(j:ka2 = g(j)) 15. h(a2) = q2   InjCase(q1; p. 1of(p), n+1of(p)) = InjCase(q2; p. 1of(p), n+1of(p))  (n+k)      a1 = a2

3 steps

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