Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
q:
.
l:
q List. enum(l)
Applied Tactic:
UnivCD THENW Auto THEN Unfold `enum` 0 THEN BLemma `nat_add` THEN Auto'
Generated subgoals:
None
q:
. l:q List. enum(l) 