is mentioned by

Thm* x1,x2:E. tree_leaf(x1) = tree_leaf(x2)  Tree(E)  x1 = x2	[tree_leaf_one_one]
Thm* E:Type, t:Tree(E). is_leaf(t)  leaf_value(t)  E	[leaf_value_wf]
Thm* E:Type, t:Tree(E). right_child(t)  Tree(E)	[right_child_wf]
Thm* E:Type, t:Tree(E). left_child(t)  Tree(E)	[left_child_wf]
Thm* E:Type, t:Tree(E). is_leaf(t)	[is_leaf_wf]
Thm* E,A:Type, l:(EA), n:(AAA), t:Tree(E). t_iterate(l;n;t)  A	[t_iterate_wf]
Thm* E:Type, x,y:Tree(E). tree_node(<x,y>)  Tree(E)	[tree_node_wf2]
Thm* E:Type, x:E. tree_leaf(x)  Tree(E)	[tree_leaf_wf2]
Thm* tree_con(E;Tree(E))  Tree(E)	[tree_subtype2]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html