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
leaf?
tree_leaf
Def tree_leaf(
x
) == inl(
x
)
Thm*
E
,
T
:Type,
x
:
E
. tree_leaf(
x
)
tree_con(
E
;
T
)
Thm*
E
:Type,
x
:
E
. tree_leaf(
x
)
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:E. tree_leaf(x) 
tree_con(E;T)E:Type, x:E. tree_leaf(x) Tree(E)E,T:Type, x:E. tree_leaf(x) tree_con(E;T)E:Type, x:E. tree_leaf(x) Tree(E)
