increasing(
x.A[(||A||-(x+1))];m)x.A[(||A||-(x+1))];m) 
s:
m. G([A[(||A||-(s+1))]]) = c List
n List)| ||s|| = 1 
& (x,y:||s||. x < y 
s[x] < s[y]) }
||L||
||L||
List
||A||
x:||A||. A[x] < n & G([A[x]]) = c
x,y:||A||. x < y A[x] > A[y]
increasing(x.A[(||A||-(x+1))];m) & (s:m. G([((x.A[(||A||-(x+1))])(s))]) = c)
| 1 | increasing(x.A[(||A||-(x+1))];m) | 1 step |
| 2 | 10. increasing(x.A[(||A||-(x+1))];m) s:m. G([A[(||A||-(s+1))]]) = c | 1 step |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |