At: phole aux 2 1 2 1 2 1 2
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. i: iii
10. j: i
11. f(i) = f(j)
i:(1+iii), j:i. f(i) = f(j)
By: InstConcl [i;j]
Generated subgoals:None
About:
