E:Type, x,y:Tree(E). tree_node( < x, y > ) 
Tree(E)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)| Who Cites node? | |
| node | Def tree_node( < x, y > ) == tree_node( < x,y > ) |
| Thm* E:Type, x,y:Tree(E). tree_node( < x, y > ) Tree(E) | |
| tree_node | Def tree_node(x) == inr(x) |
| Thm* E,T:Type, x:(TT). tree_node(x) tree_con(E;T) | |
|
Thm* E:Type, x,y:Tree(E). tree_node( < x,y > ) Tree(E) |
| Syntax: | tree_node( < x, y > ) | has structure: | node(x; y) |
About:
 |  |  |  |  |  |  |