Level:
Lib
Thy
Top
:
2
Hypotheses:
n :
m :
0 < m
k:
(n
m - 1).
l:
n List. ||l|| = m - 1
en(l) = k
Conclusion:
k:
(n
m).
l:
n List. ||l|| = m
en(l) = k
Applied Tactic:
D 0 THENW Auto
Generated subgoals:
1
.
l:
n List. ||l|| = m
en(l) = k
k:(n
m - 1). 
l:n List. ||l|| = m - 1 
en(l) = k
k:(nm). l:n List. ||l|| = m en(l) = kl:n List. ||l|| = m en(l) = k