Def en(l) == if null(l) 0 else hd(l)+en(tl(l))n fi (recursive)

Thm* n:, l:n*. en(l)

Def tl(l) == Case of l; nil nil ; h.t t

Thm* A:Type, l:A*. tl(l) A*

Def hd(l) == Case of l; nil "?" ; h.t h

Thm* A:Type, l:A*. ||l||1 hd(l) A

Def null(as) == Case of as; nil true ; a.as' false

Thm* T:Type, as:T*. null(as)

Thm* null(nil)