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]
Thm* Size(Cons(Inj(1);Cons(Inj(2);Inj(1)))) = 3	[sfa_doc_sexpr_size_example]
Thm* A:Type, C:(Sexpr(A)Type), s:Sexpr(A), Thm* f:(s1,s2:Sexpr(A)C(Cons(s1;s2))), g:(x:AC(Inj(x))). Thm* (Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1,s2))  C(s)	[sfa_doc_sexpr_cases_wf]
Thm* s:Sexpr(A). (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))	[sfa_doc_sexpr_case_thm]
Def Reverse(e) Def == Case of e Def == CaInj(x)  Inj(x) Def == CaCons(s1;s2)  Cons(Reverse(s2);Reverse(s1)) Def (recursive)	[sfa_doc_sexpr_reverse]
Def sexprCdr(s) == Case of s :  Inj(x)  Inj(x) ; Cons(s1;s2)  s2	[sfa_doc_sexpr_cdr]
Def sexprCar(s) == Case of s :  Inj(x)  Inj(x) ; Cons(s1;s2)  s1	[sfa_doc_sexpr_car]

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