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

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

Def {i..j} == {k:| i k < j }

Thm* m,n:. {m..n} Type

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

Thm* A:Type, l:A*. ||l||

Thm* ||nil||

Def == {i:| 0i }

Thm* Type

Def == {i:| 0 < i }

Thm* Type

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)

Def AB == B < A

Thm* i,j:. ij Prop

Def A == A False

Thm* A:Prop. (A) Prop