Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
q:
.
a:
.
l:
q List. enum(l) = a
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
.
l:
q List. enum(l) = a
q:
. a:. 
l:q List. enum(l) = al:q List. enum(l) = a