int_seg	Def {i..j} == {k:| i k < j} Thm* m,n:. {m..n} Type
en	Def (rec) en(l) == if null(l) 0 else hd(l)+en(tl(l))n fi Thm* n:, l:n*. en(l)
length	Def (rec) ||as|| == Case of as : null 0 ; a.as' ||as'||+1 Thm* l:A*. ||l|| Thm* ||nil||
nat_plus	Def == {i:| 0 < i} Thm* Type
lelt	Def i j < k == ij & j < k
tl	Def tl(l) == ListInd(l;nil;h,t,v.t) Thm* l:A*. tl(l) A*
hd	Def hd(l) == ListInd(l;"?";h,t,v.h) Thm* l:A*. (||l|| 1 ) hd(l) A
null	Def null(as) == Case of as : null true ; a.as' false Thm* as:T*. null(as) Thm* null(nil)
le	Def AB == B < A Thm* i,j:. ij Prop
not	Def A == A False Thm* (A) Prop