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