Who Cites t iterate?
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
case_default	Def Default => body(value,value) == body
case_tree_leaf	Def Case tree_leaf(x) => body(x) cont(x1,z) Def == InjCase(x1; x2. body(x2); _. cont(z,z))
case_node	Def Case x;y => body(x;y) cont(x1,z) Def == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0))
case	Def Case(value) body == body(value,value)

Syntax:

t_iterate(l;n;t)

has structure:

t_iterate(l; n; t)

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