Who Cites list accum?
list_accum	Def list_accum(x,a.f(x;a);y;l) Def == Case of l; nil  y ; b.l'  list_accum(x,a.f(x;a);f(y;b);l') Def (recursive)
	Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l)  T'

Syntax:

list_accum(x,a.f(x;a);y;l)

has structure:

list_accum(x,a.f(x;a); y; l)

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