At: phole aux 2 1 2 1 2 1 1 1
1. n: {2...}
2. 
f:(
n
(-1+n)). 
i:n, j:i. f(i) = f(j)
3. f: (1+n)n
4. iii: {1..(1+n)
}
5. ii:{(1+iii)..(1+n)}, jj:ii. 
f(ii) = f(jj)
6. fi: n
7. fi = f(iii)
8. x:iii. fi = f(x)
9. ii: {iii..(1+n)}
10. iii = ii 
{1..(1+n)}
jj:ii. f(ii) = f(jj)
By:
Analyze 0
THEN
Witness8 jj
THEN
Analyze 0
THEN
Analyze -2
Generated subgoals:None
About:
