Def Reverse(e)
Def == Case of e
Def == CaInj(x)  Inj(x)
Def == CaCons(s1;s2)  Cons(Reverse(s2);Reverse(s1))
Def (recursive)

is mentioned by

Thm* a,b,c:X. Thm* Reverse(Cons(Inj(a);Cons(Inj(b);Inj(c)))) Thm* = Thm* Cons(Cons(Inj(c);Inj(b));Inj(a))

[sfa_doc_sexpr_reverse_example]

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