Some definitions of interest.
append	Def as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs)  T List
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
bnot	Def b == if b false else true fi
	Thm* b:. b
deq-member	Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)
deq	Def EqDecider(T) == eq:TTx,y:T. x = y  (eq(x,y))
	Thm* T:Type. EqDecider(T)  Type
eq_int	Def i=j == if i=j true ; false fi
	Thm* i,j:. (i=j)
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
filter	Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l)
	Thm* T:Type, P:(T), l:T List. filter(P;l)  T List
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html