Nuprl - Some Definitions

nth_tl	`Def (rec) nth_tl(n;as) == if n z 0 as else nth_tl(n-1;tl(as)) fi` `Thm* as:A, i:. nth_tl(i;as) A`
tl	`Def tl(l) == ListInd(l;nil;h,t,v.t)` `Thm* l:A. tl(l) A`
le_int	`Def i z j == j < z i` `Thm* i,j:. i z j`
lt_int	`Def i < z j == if i < j true ; false fi` `Thm* i,j:. i < z j`
bnot	`Def b == if b false else true fi` `Thm* b:. b`