Some definitions of interest.
t_iterate	Def t_iterate(l;n;t) Def == Case(t) Def == Case x;y => Def == Casen(t_iterate(l;n;x),t_iterate(l;n;y)) Def == Case tree_leaf(x) => Def == Casel(x) Def == Default => True Def (recursive)
	Thm* E,A:Type, l:(EA), n:(AAA), t:Tree(E). t_iterate(l;n;t)  A
tree	Def Tree(E) == rec(T.tree_con(E;T))
	Thm* E:Type. Tree(E)  Type

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