Who Cites reverse?
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

Syntax:

rev(as)

has structure:

reverse(as)

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