Level: Lib Thy Top: 2
Hypotheses:

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

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

  3. f : (n + 1) n

Conclusion:

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

Applied Tactic: Assert iii:(n + 1) (ii:{(iii + 1)..(n + 1)}. jj:ii. (f ii = f jj)) (i:(iii + 1). j:i. f i = f j)
Generated subgoals:

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

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