Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

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

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

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