Some definitions of interest.
reverse	Def rev(as) == Case of as; nil  nil ; a.as'  rev(as') @ [a]  (recursive)
	Thm* T:Type, as:T List. rev(as)  T List
append	Def as @ bs == Case of as; nil  bs ; a.as'  a.(as' @ bs)  (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs)  T List
subtype	Def S  T == x:S. x  T

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