Def rev(as) == Case of as; nil  nil ; a.as'  rev(as') @ [a]  (recursive)

is mentioned by

Thm* as,bs:T List. rev(as @ bs) = (rev(bs) @ rev(as))

[reverse_append]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html