WhoCites
Definitions
mb
tree
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites tree
node?
tree_node
Def tree_node(
x
) == inr(
x
)
Thm*
E
,
T
:Type,
x
:(
T
T
). tree_node(
x
)
tree_con(
E
;
T
)
Thm*
E
:Type,
x
,
y
:Tree(
E
). tree_node(<
x
,
y
>)
Tree(
E
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
tree
Sections
MarkB
generic
Doc
E,T:Type, x:(T
T). tree_node(x) 
tree_con(E;T)E:Type, x,y:Tree(E). tree_node(<x,y>) Tree(E)E,T:Type, x:(TT). tree_node(x) tree_con(E;T)E:Type, x,y:Tree(E). tree_node(<x,y>) Tree(E)
