Some definitions of interest.
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
iff	Def P  Q == (P  Q) & (P  Q)
	Thm* A,B:Prop. (A  B)  Prop
sublist	Def L1  L2 Def == f:(||L1||||L2||).  Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)
	Thm* T:Type, L1,L2:T List. L1  L2  Prop
not	Def A == A  False
	Thm* A:Prop. (A)  Prop
null	Def null(as) == Case of as; nil  true ; a.as'  false
	Thm* T:Type, as:T List. null(as)
	Thm* null(nil)
tl	Def tl(l) == Case of l; nil  nil ; h.t  t
	Thm* A:Type, l:A List. tl(l)  A List

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