t:Label. t 
SimpleTypeE,T:Type, x:E. tree_leaf(x) tree_con(E;T)E:Type, x:E. tree_leaf(x) Tree(E)| Who Cites typ? | |
| typ | Def t == tree_leaf(inl(t)) |
| Thm* t:Label. t SimpleType | |
| tree_leaf | Def tree_leaf(x) == inl(x) |
| Thm* E,T:Type, x:E. tree_leaf(x) tree_con(E;T) | |
| Thm* E:Type, x:E. tree_leaf(x) Tree(E) |
| Syntax: | t | has structure: | typ(t) |
About:
 |  |  |  |  |