Def enum(l) == (q||l||)+en(l)

Thm* q:, l:q*. enum(l)

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

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

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

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

Thm* ||nil||

Def (qn) == if n=0 0 else (qn-1)+(qn-1) fi (recursive)

Thm* q,n:. (qn)

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 (basepower) == if power=0 1 else base(basepower-1) fi (recursive)

Thm* n,k:. (nk)

Thm* n,k:. (nk)

Def i=j == if i=j true ; false fi

Thm* i,j:. i=j