E:Type. Tree(E) 
Type
T)E,T:Type. tree_con(E;T) Type| Who Cites tree? | |
| tree | Def Tree(E) == rec(T.tree_con(E;T)) |
| Thm* E:Type. Tree(E) Type | |
| tree_con | Def tree_con(E;T) == E+(TT) |
| Thm* E,T:Type. tree_con(E;T) Type |
| Syntax: | Tree(E) | has structure: | tree(E) |
About:
 |  |  |  |  |  |  |