e:
, L:*, n:
. ||e:(L
n)|| = n
||e:L|| 
counter_lpower
0 ;e=
hd(L)1+||e:tl(L)|| else ||e:tl(L)|| fi
(recursive)
Thm* e:, L:*, n:. ||e:(Ln)|| = n||e:L|| counter_lpower
Thm* e:, L,M:*. ||e:L @ M|| = ||e:L||+||e:M|| counter_append
Thm* e:. ||e:nil|| = 0 counter_of_nil