Some definitions of interest.
sfa_doc_inlist	Def a list xs == Case of xs; nil  False ; x.ys  x = a  A  a list ys Def (recursive)
	Thm* A:Type, a:A, xs:A List. (a list xs)  Prop
singleton	Def {a:T} == {x:T| x = a  T }
	Thm* T:Type, a:T. {a:T}  Type

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