Some definitions of interest.
nat_plus	Def  == {i:| 0<i }
	Thm*   Type
nequal	Def a  b  T == a = b  T
	Thm* A:Type, x,y:A. (x  y)  Prop
sfa_doc_sexpr	Def Sexpr(A) == rec(T.(TT)+A)
	Thm* A:Type. Sexpr(A)  Type
sfa_doc_sexpr_cdr	Def sexprCdr(s) == Case of s :  Inj(x)  Inj(x) ; Cons(s1;s2)  s2
	Thm* A:Type, s:Sexpr(A). sexprCdr(s)  Sexpr(A)
sfa_doc_sexpr_cons	Def Cons(s1;s2) == inl(<s1,s2>)
	Thm* A:Type, s1,s2:Sexpr(A). Cons(s1;s2)  Sexpr(A)
sfa_doc_sexpr_size	Def Size(s) == Case of s :  Inj(x)  1 ; Cons(s1;s2)  Size(s1)+Size(s2) Def (recursive)
	Thm* A:Type, s:Sexpr(A). Size(s)

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