Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: (BLemma `int_upper_ind` THENM RepD ...a)
Generated subgoals:

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

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