Level: Lib Thy Top: 2
Hypotheses:

  1. n : {1 + 1...}

  2. f:((n - 1) + 1) (n - 1). i:((n - 1) + 1). j:{(i + 1)..((n - 1) + 1)}. f i = f j

  3. f : (n + 1) n

Conclusion:

i:(n + 1). j:{(i + 1)..(n + 1)}. f i = f j

Applied Tactic: (OnMCls [1;2;0] ArithSimp ...a) THEN (Decide k:n. f n = f k ...a)
Generated subgoals:

1. i:(1 + n). j:{(1 + i)..(1 + n)}. f i = f j

2. i:(1 + n). j:{(1 + i)..(1 + n)}. f i = f j