Def Sexpr(A) == rec(T.(TT)+A)

is mentioned by

Thm* A:Type. Sexpr(A) =ext (Sexpr(A)Sexpr(A))+A	[sfa_doc_sexpr_fp]
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* A:Type, e:Sexpr(A). Reverse(e)  Sexpr(A)	[sfa_doc_sexpr_reverse_wf]
Thm* A:Type, s:Sexpr(A). Size(s) = 1    sexprAtom(s)  A	[sfa_doc_sexpr_atom_wf]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCdr(s))<Size(s)	[sfa_doc_sexprcdrsize]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCar(s))<Size(s)	[sfa_doc_sexprcarsize]
Thm* A:Type, s:Sexpr(A). Size(s)	[sfa_doc_sexpr_size_wf]
Thm* A:Type, s:Sexpr(A). sexprCdr(s)  Sexpr(A)	[sfa_doc_sexpr_cdr_wf]
Thm* A:Type, s:Sexpr(A). sexprCar(s)  Sexpr(A)	[sfa_doc_sexpr_car_wf]
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]
Thm* A:Type, a:A. Inj(a)  Sexpr(A)	[sfa_doc_sexpr_inj_wf]
Thm* A:Type, s1,s2:Sexpr(A). Cons(s1;s2)  Sexpr(A)	[sfa_doc_sexpr_cons_wf]

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html