Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
n:
.
l:
n List. en(l)
Applied Tactic:
UnivCD THENW Auto THEN ListInd 2 THEN RecUnfold `en` 0 THEN Reduce 0
Generated subgoals:
1
. 0
2
. u + en(v) * n
n:
. l:n List. en(l) 