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 tree node? | |
| 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) |
About:
 |  |  |  |  |  |  |