Def Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1;s2)
Def == InjCase(s; s1s2. s1s2/s1,s2. f(s1;s2); x. g(x))

is mentioned by

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 sexprAtom(s) == Case of s :  Inj(x)  x ; Cons(s1;s2)  0	[sfa_doc_sexpr_atom]
Def Size(s) == Case of s :  Inj(x)  1 ; Cons(s1;s2)  Size(s1)+Size(s2) Def (recursive)	[sfa_doc_sexpr_size]
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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html