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
exists_unique	Def  !x:A. P(x) == x:A. x is the x:A. P(x)
	Thm*  A:Type, P:(AProp). (!x:A. P(x))  Prop
iff	Def  P  Q == (P  Q) & (P  Q)
	Thm*  A,B:Prop. (A  B)  Prop
is_the	Def  x is the u:A. P(u) == P(x) & (u:A. P(u)  u = x)
	Thm*  A:Type, P:(AProp), x:A. (x is the x:A. P(x))  Prop

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