Some definitions of interest.
sfa_doc_sexpr	Def Sexpr(A) == rec(T.(TT)+A)
	Thm* A:Type. Sexpr(A)  Type
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_inj	Def Inj(a) == inr(a)
	Thm* A:Type, a:A. Inj(a)  Sexpr(A)

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