Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
L:T List. 0 < ||L||
L = (hd(L)::tl(L))
Applied Tactic:
(D 0 THENM D 0 THENM ListInd 2 THENM Reduce 0 ...)
Generated subgoals:
None
T:
. L:T List. 0 < ||L|| 
L = (hd(L)::tl(L))