2 | 19. c@0: ||L[c--]|| 20. f@0:( L[c--][c@0]  R[c]).
increasing(f@0;L[c--][c@0])
& ( s: L[c--][c@0] List.
||s|| = k  ( x,y: ||s||. x < y  s[x] < s[y])  G(map(f;map(f@0;s))) = c@0) 21. c@0 ||L|| 22. c1: ||L|| 23. f1: L[c1]  n 24. increasing(f1;L[c1]) 25. s: L[c1] List 26. ||s|| = k  27. x,y: ||s||. x < y  s[x] < s[y] map(f1;s) {s:( n List)| ||s|| = k & ( x,y: ||s||. x < y  s[x] < s[y]) } | 1 step |