T:Type, i,j:.
  i<j
  
  (f:(T), P:(T).
  (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)

By:

Auto THEN Inst Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n))) [j;i] THEN HypSubst -1 0 THEN RWO Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as')) 0 THEN RWO Thm* P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B)) 0 THEN GenConcl ((x.x+i) = addi) THEN RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   0

1

1. T : Type 2. i :  3. j :  4. i<j 5. f : T 6. P : T 7. P(f(i)) 8. upto(j) ~ (upto(i) @ map(x.x+i;upto(j-i))) 9. addi :  10. (x.x+i) = addi   ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(i)))||   +||filter(P;map(f;map(addi;upto(j-i))))||

6 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html