Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:
. m:. k:(n
m). 
l:n List. ||l|| = m 
en(l) = k
Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto THEN NatInd 2
Generated subgoals:1. k:(n0). l:n List. ||l|| = 0 en(l) = k2. k:(nm). l:n List. ||l|| = m en(l) = k