Level:
Lib
Thy
Top
:
1
Hypotheses:
n : {1...}
m : {n + 1...}
f :
m
n
Conclusion:
i,j:
m. i < j
f i = f j
Applied Tactic:
InstLemma `phole_aux` [
n
;
f
] THENW Auto
Generated subgoals:
1
.
i,j:
m. i < j
f i = f j
m 
n
i,j:m. i < j 
f i = f j
n
;f] THENW Autoi,j:m. i < j f i = f j