Level: Lib Thy Top: 1
Hypotheses:

  1. e :

Conclusion:

||e:[]|| = 0

Applied Tactic: RW (RecUnfoldC `el_counter`) 0 THEN AbReduce 0 THEN Auto
Generated subgoals:

None