Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:
. m:. l1,l2:n List. ||l1|| = m 
||l2|| = m 
en(l1) = en(l2) l1 = l2
Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto
Generated subgoals:1. l1,l2:n List. ||l1|| = m ||l2|| = m en(l1) = en(l2) l1 = l2