Some definitions of interest.
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
decidable	Def Dec(P) == P  P
	Thm* A:Prop. Dec(A)  Prop
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
swap_adjacent	Def swap adjacent[P(x;y)](L1,L2) Def == i:(||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1)  A List
	Thm* A:Type, P:(AAProp). swap adjacent[P(x,y)]  (A List)(A List)Prop
int_seg	Def {i..j} == {k:| i  k < j }
	Thm* m,n:. {m..n}  Type
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
rel_star	Def (R^*)(x,y) == n:. x R^n y
	Thm* T:Type, R:(TTProp). (R^*)  TTProp
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
select	Def l[i] == hd(nth_tl(i;l))
	Thm* A:Type, l:A List, n:. 0n  n<||l||  l[n]  A

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