Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
q:
.
l1,l2:
q List. enum(l1) = enum(l2)
l1 = l2
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
. l1 = l2
q:
. l1,l2:q List. enum(l1) = enum(l2) 
l1 = l2