At:
Ramsey-base-case
1
2
1
1
1
1
1.
L: 
List
2.
n:
3.
sum(L[i]-1 | i < ||L||)+1
n
4.
G: {s:(n List)| ||s|| = 1 
& (
x,y:||s||. x < y 
s[x] < s[y]) }
||L||
5.
c: ||L||
6.
f: L[c]n
7.
increasing(f;L[c])
8.
s:L[c]. G([(f(s))]) = c
9.
increasing(f;L[c])
10.
u: L[c]
11.
1 = 1
12.
x,y:1. x < y [u][x] < [u][y]
G([(f(u))]) = c
By:
EasyHyp
Generated subgoals:
None
About:
