Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
n:{1...}.
m:{n + 1...}.
f:
m
n.
i,j:
m. i < j
f i = f j
Applied Tactic:
GenUnivCD THENW Auto
Generated subgoals:
1
.
i,j:
m. i < j
f i = f j
n:{1...}. m:{n + 1...}. f:
m 
n. 
i,j:m. i < j 
f i = f ji,j:m. i < j f i = f j