Who Cites for hdtl?
for_hdtl	Def ForHdTl{A,f,k} h::t  as. g(h;t) == reduce(f;k;mapcons(h,t. g(h;t);as))
	Thm* A,B,C:Type, f:(BCC), k:C, as:A List, g:(A(A List)B). Thm* (ForHdTl{A,f,k} h::t  as. g(h,t))  C
mapcons	Def mapcons(f;as) == Case of as; nil  nil ; a.as'  f(a,as').mapcons(f;as') Def (recursive)
	Thm* A,B:Type, f:(A(A List)B), l:A List. mapcons(f;l)  B List
reduce	Def reduce(f;k;as) == Case of as; nil  k ; a.as'  f(a,reduce(f;k;as')) Def (recursive)
	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as)  B

Syntax:

ForHdTl{A,f,k} h::t  as. g(h;t)

has structure:

for_hdtl(A; f; k; as; h,t.g(h;t))

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