Level:
Lib
Thy
Top
:
1
1
Hypotheses:
n : {1...}
m : {n + 1...}
f :
m
n
i:
(n + 1).
j:
i. f i = f j
Conclusion:
i,j:
m. i < j
f i = f j
Applied Tactic:
ExRepD
Generated subgoals:
1
.
i,j:
m. i < j
f i = f j
m 
n
i:(n + 1). j:i. f i = f j
i,j:m. i < j 
f i = f ji,j:m. i < j f i = f j