))
SimpleType
E,T:Type, x:E. tree_leaf(x) tree_con(E;T)E:Type, x:E. tree_leaf(x) Tree(E)| Who Cites st top? | |
| st_top | Def tTop == tree_leaf(inr()) |
| Thm* tTop 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: | tTop | has structure: | st_top |
About:
 |  |  |  |  |  |  |