n:
, m:, k:(n
m). 
l:n*. ||l|| = m & en(l) = k en_surj
0 else hd(l)+en(tl(l))
n fi (recursive)
Thm* n:, m:, k:(nm). l:n*. ||l|| = m & en(l) = k en_surj
Thm* n:, l:n*. en(l) 
(n||l||) en_bound
Thm* n:, l:n*. en(l) < (n||l||) en_ubound
Thm* n:, m:, l1,l2:n*. ||l1|| = m & ||l2|| = m 
en(l1) = en(l2) l1 = l2
en_inj