Some definitions of interest.
length	Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
unzip	Def unzip(as) == <map(p.1of(p);as),map(p.2of(p);as)>
	Thm* T1,T2:Type, as:(T1T2) List. unzip(as)  (T1 List)(T2 List)
map	Def map(f;as) == Case of as; nil  nil ; a.as'  [(f(a)) / map(f;as')] Def (recursive)
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
	Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
zip	Def zip(as;bs) Def == Case of as Def == Canil  nil Def == Caa.as'  Case of bs; nil  nil ; b.bs'  [<a,b> / zip(as';bs')] Def (recursive)
	Thm* T1,T2:Type, as:T1 List, bs:T2 List. zip(as;bs)  (T1T2) List

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