b == tree_node( < a, b > )
a,b:SimpleType. ab 
SimpleTypeE: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 arrow? | |
| arrow | Def ab == tree_node( < a, b > ) |
| Thm* a,b:SimpleType. ab SimpleType | |
| 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: | ab | has structure: | arrow(a; b) |
About:
 |  |  |  |  |  |  |