t1,t2:Term. t1 t2 
TermE: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 tapp? | |
| tapp | Def t1 t2 == tree_node( < t1, t2 > ) |
| Thm* t1,t2:Term. t1 t2 Term | |
| 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: | t1 t2 | has structure: | tapp(t1; t2) |
About:
 |  |  |  |  |  |  |