Who Cites t iterate?
t_iterate	Def t_iterate(l;n;t) == Case(t) Case x;y = > n(t_iterate(l;n;x),t_iterate(l;n;y)) Case tree_leaf(x) = > l(x) Default = > True (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) == InjCase(x1; x2. body(x2); _. cont(z,z))
case_node	Def Case x;y = > body(x;y) cont(x1,z) == 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: