2 | 18. G:({s:( R[c] List)| ||s|| = k & ( x,y: ||s||. x < y  s[x] < s[y]) }  ||L[c--]||).
c@0: ||L[c--]||, f:( L[c--][c@0]  R[c]).
increasing(f;L[c--][c@0])
& ( s: L[c--][c@0] List. ||s|| = k  ( x,y: ||s||. x < y  s[x] < s[y])  G(map(f;s)) = c@0) 19. ( s. G(map(f;s))) {s:( R[c] List)| ||s|| = k & ( x,y: ||s||. x < y  s[x] < s[y]) }  ||L[c--]|| c: ||L||, f:( L[c]  n). increasing(f;L[c]) & ( s: L[c] List. ||s|| = k  ( x,y: ||s||. x < y  s[x] < s[y])  G(map(f;s)) = c) | 73 steps |