Level: Lib Thy Top: 2 1
Hypotheses:- n : {1 + 1...}
f:
((n - 1) + 1) 
(n - 1). 
i:((n - 1) + 1). j:i. f i = f j- f : (n + 1) n
Conclusion:
iii:(n + 1)
(ii:{(iii + 1)..(n + 1)
}. jj:ii. 
(f ii = f jj)) 
(i:(iii + 1). j:i. f i = f j)
Applied Tactic: (BLemma `int_seg_ind` THENM All ArithSimp ...a)
Generated subgoals:1. (ii:{1..(1 + n)}. jj:ii. (f ii = f jj)) (i:1. j:i. f i = f j)2. iii:{1..(1 + n)}
((ii:{iii..(1 + n)}. jj:ii. (f ii = f jj)) (i:iii. j:i. f i = f j))
(ii:{(1 + iii)..(1 + n)}. jj:ii. (f ii = f jj))
(i:(1 + iii). j:i. f i = f j)